Research proof index

Restriction commutes with the “right-anchored infimum” construction μmin from Basic.lean. This is the dual statement to μmax_res_intvl.

Existence theorem packaging the lexicographic construction. It produces a LinearOrder (Finset α) with two convenient properties: 1. Subset-monotonicity: A ⊆ B implies A ≤ B. 2. Singleton compatibility: comparing singleton finsets recovers the original order on α. API note: returning the order via ∃ lo allows users to avoid a global instance and...

Universal property (extension) for the Dedekind–MacNeille completion. Given an order embedding f : α ↪o β into a complete lattice β, this theorem produces an order embedding f' : DedekindMacNeilleCompletion α ↪o β such that f = f' ∘ coe'. API note: the constructed f' is defined by a sSup over lower bounds of upper bounds of the image of x. T...