Structures · Topology
OrderClosedTopology
A topology on a set which is both a topological space and a preorder is _order-closed_ if the
set of points (x, y) with x ≤ y is closed in the product space. We introduce this as a mixin.
This property is satisfied for the order topology on a linear order, but it can be satisfied more
generally, and suffices to derive many interesting properties relating order and topology.
- Defined in
- Mathlib.Topology.Order.OrderClosed
- Shape
- One type argument · adds isClosed_le'
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances3
- Subtype
- Prod
- OrderDual
How is a type an instance?
Loading the hierarchy index…
Assumed by454
- isOpen_Ioo
- measurableSet_Ioo
- measurableSet_Icc
- isClosed_le
- measurableSet_le
- Ioo_mem_nhds
- Summable.tsum_le_tsum
- isOpen_lt
- Icc_mem_nhds
- measurableSet_lt
- le_of_tendsto_of_tendsto'
- tsum_nonneg
- isClosed_Icc
- Summable.sum_le_tsum
- le_of_tendsto_of_tendsto
- hasSum_le
- MeasureTheory.setIntegral_mono_set
- MeasureTheory.StronglyMeasurable.measurableSet_le
- Monotone.ge_of_tendsto
- Summable.tsum_le_of_sum_le
- OrderClosedTopology.isClosed_le'
- Continuous.max
- isLUB_of_tendsto_atTop
- sum_le_hasSum
- Antitone.le_of_tendsto
- Summable.le_tsum
- cocompact_eq_atBot_atTop
- MeasureTheory.aecover_Ioo_of_Ioo
- IsPreconnected.intermediate_value
- hasProd_le
- closure_lt_subset_le
- frontier_le_subset_eq
- ProperCone.positive
- nullMeasurableSet_lt
- MeasureTheory.aecover_Ioi
- ContinuousOn.image_Icc_of_monotoneOn
- Summable.tsum_le_tsum_of_inj
- Filter.Tendsto.min
- Continuous.min
- Dense.exists_between
- intermediate_value_univ₂
- ContinuousWithinAt.closure_le
- Summable.tsum_lt_tsum
- MeasureTheory.integral_mono_measure
- le_hasSum
- Measurable.max
- isClosed_le_prod
- continuous_if_le
- IsClosed.isClosed_le
- IsPreconnected.Icc_subset
Ancestors0
No ancestors.