Structures · Order
LocallyFiniteOrderBot
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
- Shape
- One type argument · adds finsetIio, finsetIic, finset_mem_Iic, finset_mem_Iio
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 by322
- Finset.Iic
- Finset.Iio
- partialSups
- disjointed
- Preorder.frestrictLe
- Finset.mem_Iic
- Finset.coe_Iic
- Finset.coe_Iio
- InnerProductSpace.gramSchmidt
- disjoint_disjointed
- Preorder.frestrictLe₂
- Finset.mem_Iio
- IicProdIoc
- Finset.nonempty_Iic
- Preorder.measurable_frestrictLe
- iUnion_disjointed
- disjointed_subset
- InnerProductSpace.gramSchmidtNormed
- Preorder.measurable_frestrictLe₂
- Finset.Ioc_subset_Iic_self
- InnerProductSpace.gramSchmidtOrthonormalBasis
- Set.finite_Iic
- Finset.Iic_subset_Iic
- measurable_IicProdIoc
- Monotone.partialSups_eq
- partialSups_apply
- Finset.notMem_Iio_self
- Set.infinite_iff_exists_gt
- disjointed_le
- LDL.lowerInv
- InnerProductSpace.gramSchmidt_orthogonal
- partialSups_disjointed
- Finset.Iic_eq_cons_Iio
- InnerProductSpace.gramSchmidt_def
- le_partialSups
- Set.Infinite.exists_gt
- InnerProductSpace.mem_span_gramSchmidt
- Finset.subset_Iic_sup_id
- partialSups_eq_biSup
- le_partialSups_of_le
- InnerProductSpace.gramSchmidt_mem_span
- Set.finite_Iio
- map_partialSups
- Finset.sup_Iic
- partialSups_succ
- Finset.card_Iio_eq_card_Iic_sub_one
- Finset.disjoint_Ioi_Iio
- disjointed_apply
- partialSups_le_iff
- Equiv.IicFinsetSet
Ancestors0
No ancestors.