Research proof index

An isomorphism rewriting a quotient by ker_of_quot_comp_localization. This lemma constructs a LinearEquiv identifying I.val.2 / ker_of_quot_comp_localization I with a quotient of I.val.2 / I.val.1 by the kernel of the localization map CP.f1 I. It is a technical step toward computing the associated primes of the intermediate quotient used in the...

Paper Lemma 2.4 (part 2) localized to an interval I. Assuming convexity of μ on I, this gives a bound between two μmax values obtained from a non-comparable pair x,w. API note: the conclusion is stated as an inequality between μmax on two strict pairs in ℒ.

Paper Lemma 2.4 (part 3) localized to an interval I. This combines lem2d4₁ and lem2d4₂I to compare μA values on two different intervals determined by the non-comparable pair x,w.

In a nontrivial totally ordered real vector space, the coercion of any vector is strictly below ⊤ in the Dedekind–MacNeille completion. This lemma is used to derive contradictions when an equality forces a coerced value to be ⊤.

Proposition 2.6 (c): a case split yielding either equality or a strict inequality chain. The hypothesis allows either comparability of the two adjacent μA values, or attainment of the infimum defining μA (x,z). The conclusion then provides a dichotomy between equality and a strict improvement.

Proposition 2.8 (auxiliary step): a disjunction bounding one of two μA values by a μmax value. This is an interval-local statement used to derive the “meet” inequality in Proposition 2.8.