Theorems · Inductive type · order theory
CompleteLinearOrder
Type u_8 → Type u_8
A complete linear order is a linear order whose lattice structure is complete.
- Defined in
- Mathlib.Order.CompleteLattice.Defs
- Cited by
- 126 results in Mathlib
- Foundations
- Depth 0 from the axioms, rests on 1 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by141
Results whose statement or proof uses this declaration.
- lt_iSup_iffstatement and proof · cited by 8
- iSup_eq_topstatement and proof · cited by 7
- sInf_lt_iffstatement and proof · cited by 7
- iInf_eq_botstatement and proof · cited by 5
- iInf₂_eq_botstatement and proof · cited by 4
- Pi.Lex.sInf_applystatement and proof · cited by 4
- lowerSemicontinuousWithinAt_iSupstatement and proof · cited by 4
- limsup_eq_botstatement and proof · cited by 3
- Monotone.map_sSup_of_continuousAtstatement and proof · cited by 3
- MonotoneOn.map_sSup_of_continuousWithinAtstatement and proof · cited by 3
- sSup_ne_of_notMemstatement and proof · cited by 3
- lowerSemicontinuousWithinAt_iff_le_liminfstatement and proof · cited by 3