Structures · Order
DenselyOrdered
An order is dense if there is an element between any pair of distinct comparable elements.
- Defined in
- Mathlib.Order.Basic
- Shape
- One type argument · adds dense
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances20
- NNReal
- ENNReal
- Units
- EReal
- DedekindCut
- Order.Fill
- Subtype
- Prod
- OrderDual
- Set.Elem
- PUnit
- Lex
- WithTop
- WithBot
- Colex
- Sum
- Multiplicative
- Additive
- Sigma
- WithZero
How is a type an instance?
Loading the hierarchy index…
Assumed by476
- exists_between
- StieltjesFunction.measure
- interior_Icc
- Set.nonempty_Ioo
- le_of_forall_gt_imp_ge_of_dense
- closure_Ioo
- exists_seq_strictAnti_tendsto
- le_of_forall_pos_le_add
- interior_Ici
- le_of_forall_lt_imp_le_of_dense
- interior_Ici'
- interior_Ico
- closure_Ioi
- BoundedVariationOn.vectorMeasure
- interior_Iic'
- interior_Ioc
- exists_seq_strictAnti_tendsto'
- Set.OrdConnected.isPreconnected
- StieltjesFunction.measure_Iic
- StieltjesFunction.measure_Ioc
- StieltjesFunction.measure_Icc
- exists_between'
- DenselyOrdered.dense
- isLUB_Ioo
- isPreconnected_Icc
- BoundedVariationOn.vectorMeasure_Icc
- interior_Iic
- isPreconnected_Ioo
- exists_seq_strictMono_tendsto'
- StieltjesFunction.measure_singleton
- ContinuousOn.image_Icc_of_monotoneOn
- StieltjesFunction.measure_univ
- closure_Iio'
- isGLB_Ioo
- closure_Ioi'
- Dense.exists_between
- isPreconnected_Ioc
- closure_Ioc
- closure_Iio
- csInf_Ioo
- isPreconnected_Ici
- closure_Ico
- le_iff_forall_pos_le_add
- Filter.limsup_le_iff'
- frontier_Ici
- continuousWithinAt_right_of_monotoneOn_of_closure_image_mem_nhdsWithin
- intermediate_value_Icc
- nhds_bot_basis_Iic
- eq_of_le_of_forall_lt_imp_le_of_dense
- csInf_Ioi
Ancestors0
No ancestors.