Structures · Order
LocallyFiniteOrder
This is a mixin class describing a locally finite order,
that is, is an order where bounded intervals are finite.
When you don't care too much about definitional equality, you can use LocallyFiniteOrder.ofIcc or
LocallyFiniteOrder.ofFiniteIcc to build a locally finite order from just Finset.Icc.
- Defined in
- Mathlib.Order.Interval.Finset.Defs
- Shape
- One type argument · adds finsetIcc, finsetIco, finsetIoc, finsetIoo, finset_mem_Icc, finset_mem_Ico, finset_mem_Ioc, finset_mem_Ioo
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances19
- Int
- Nat
- Units
- Finsupp
- DFinsupp
- PNat
- Subtype
- Prod
- OrderDual
- Fin
- Lex
- WithTop
- WithBot
- Sum
- Multiplicative
- Additive
- Sigma
- Multiset
- Finset
How is a type an instance?
Loading the hierarchy index…
Assumed by735
- Finset.Ico
- Finset.Icc
- Finset.Ioc
- Finset.Ioo
- Finset.uIcc
- Finset.coe_Ico
- Finset.coe_Icc
- Finset.coe_Ioc
- Finset.mem_Ico
- Finset.coe_Ioo
- Finset.mem_Icc
- Multiset.Ico
- Finset.mem_Ioc
- Finset.Ico_eq_empty_of_le
- IicProdIoc
- SummationFilter.symmetricIco
- SummationFilter.symmetricIcc
- IncidenceAlgebra.mu
- Multiset.Icc
- Finset.right_notMem_Ico
- Finset.coe_uIcc
- SummationFilter.conditional
- Finset.mem_Ioo
- Multiset.Ioo
- Set.finite_Icc
- Finset.Icc_self
- Finset.Ioc_subset_Iic_self
- Finset.box
- Multiset.Ioc
- Finset.Ico_add_one_right_eq_Icc
- measurable_IicProdIoc
- Finset.card_Ico_eq_card_Icc_sub_one
- Finset.Ico_subset_Ico
- Finset.left_notMem_Ioc
- Finset.insert_Ico_right_eq_Ico_add_one
- Finset.Ico_self
- Finset.Ico_union_Ico_eq_Ico
- HahnSeries.ofSuppBddBelow
- Finset.Icc_eq_cons_Ico
- Finset.sum_Ico_add'
- LocallyFiniteOrder.addMonoidHom
- Finset.left_notMem_Ioo
- Finset.card_Ioo_eq_card_Icc_sub_two
- Finsupp.rangeIcc
- DFinsupp.card_Icc
- Finset.Icc_subset_Icc
- Finset.card_Ioc_eq_card_Icc_sub_one
- Finset.Icc_eq_cons_Ioc
- Finsupp.card_Icc
- Finset.Ioc_eq_empty_of_le
Ancestors0
No ancestors.