Structures · Order
LocallyFiniteOrderTop
This mixin class describes an order where all intervals bounded below are finite. This is
slightly weaker than LocallyFiniteOrder + OrderTop as it allows empty types.
- Defined in
- Mathlib.Order.Interval.Finset.Defs
- Shape
- One type argument · adds finsetIoi, finsetIci, finset_mem_Ici, finset_mem_Ioi
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances7
- Subtype
- Prod
- OrderDual
- Fin
- Lex
- Sum
- Sigma
How is a type an instance?
Loading the hierarchy index…
Assumed by132
- Finset.Ioi
- Finset.Ici
- Finset.coe_Ioi
- Finset.coe_Ici
- Finset.mem_Ici
- Finset.mem_Ioi
- Finset.notMem_Ioi_self
- Finset.Ioi_eq_empty
- Finset.Ici_eq_cons_Ioi
- Finset.disjoint_Ioi_Iio
- BddBelow.finite
- Finset.filter_le_eq_Ici
- Finset.nonempty_Ici
- LocallyFiniteOrderTop.finset_mem_Ici
- Finset.Ici_succ_eq_Ioi_of_not_isMax
- Multiset.Ici
- Finset.Ici_succ_eq_Ioi
- Set.finite_Ici
- Finset.prod_prod_Ioi_mul_eq_prod_prod_off_diag
- LocallyFiniteOrderTop.finsetIoi
- Finset.card_Ioi_eq_card_Ici_sub_one
- Finset.Ioi_pred_eq_Ici_of_not_isMin
- Finset.Ico_subset_Ici_self
- Set.toFinset_Ici
- Finset.Ioi_pred_eq_Ici
- Finset.Ioi_insert
- LocallyFiniteOrderTop.finset_mem_Ioi
- Pi.card_Ici
- Finset.mul_prod_Ioi_eq_prod_Ici
- LocallyFiniteOrderTop.finsetIci
- Finset.nonempty_Ioi
- Finset.Ioi_disjUnion_Iio
- Set.Infinite.not_bddBelow
- Finset.subtype_Ioi_eq
- Finset.inf_Ici
- Finset.subtype_Ici_eq
- Set.Infinite.exists_lt
- Multiset.Ioi
- Finset.Icc_subset_Ici_self
- Finset.add_sum_Ioi_eq_sum_Ici
- Finset.Ici_add_Ioi_subset
- Set.infinite_iff_exists_lt
- Sum.Lex.Ici_inr
- Sum.Ici_inl
- Finset.Ioo_subset_Ici_self
- Sum.Lex.instLocallyFiniteOrderTop
- Finset.Iic_toDual
- Sum.Lex.Ioo_inl_inl
- Finset.Ioi_add_Ici_subset
- Finset.Ioi_ofDual
Ancestors0
No ancestors.