Theorems · Inductive type · order theory
LocallyFiniteOrderBot
(α : Type u_1) → [Preorder α] → Type u_1
This mixin class describes an order where all intervals bounded above are finite. This is
slightly weaker than LocallyFiniteOrder + OrderBot as it allows empty types.
- Defined in
- Mathlib.Order.Interval.Finset.Defs
- Cited by
- 286 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
- Assumes
- Preorder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Preorderstatement · cited by 7,952
Cited by321
Results whose statement or proof uses this declaration.
- Finset.Iicstatement and proof · cited by 280
- Finset.Iiostatement and proof · cited by 147
- partialSupsstatement and proof · cited by 67
- disjointedstatement and proof · cited by 64
- Preorder.frestrictLestatement and proof · cited by 43
- Finset.mem_Iicstatement and proof · cited by 42
- Finset.coe_Iicstatement and proof · cited by 36
- Finset.coe_Iiostatement and proof · cited by 34
- InnerProductSpace.gramSchmidtstatement and proof · cited by 30
- disjoint_disjointedstatement and proof · cited by 25
- Preorder.frestrictLe₂statement and proof · cited by 23
- Finset.mem_Iiostatement and proof · cited by 20
Showing the 200 most cited of 321.