Structures · Topology
ContinuousInf
Let L be a topological space and let L×L be equipped with the product topology and let
⊓:L×L → L be an infimum. Then L is said to have (jointly) continuous infimum if the map
⊓:L×L → L is continuous.
- Defined in
- Mathlib.Topology.Order.Lattice
- Shape
- One type argument · adds continuous_inf
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances1
- OrderDual
How is a type an instance?
Loading the hierarchy index…
Assumed by58
- MeasureTheory.AEEqFun.coeFn_inf
- Filter.Tendsto.inf_nhds'
- MeasureTheory.StronglyMeasurable.inf
- ContinuousMap.inf'_apply
- Filter.Tendsto.finset_inf'_nhds_apply
- Filter.Tendsto.finset_inf_nhds_apply
- ContinuousAt.finset_inf'_apply
- ContinuousAt.finset_inf_apply
- ContinuousWithinAt.finset_inf'_apply
- ContinuousWithinAt.finset_inf_apply
- continuous_inf
- ContinuousWithinAt.inf'
- MeasureTheory.AEStronglyMeasurable.inf
- Filter.Tendsto.inf_nhds
- Continuous.inf
- ContinuousAt.inf'
- MeasureTheory.FinStronglyMeasurable.inf
- ContinuousWithinAt.finset_inf'
- ContinuousAt.finset_inf
- ContinuousAt.finset_inf'
- ContinuousInf.continuous_inf
- ContinuousOn.inf'
- ContinuousWithinAt.finset_inf
- CompactlySupportedContinuousMap.finsetInf'_apply
- MeasureTheory.AEEqFun.le_inf
- CompactlySupportedContinuousMap.coe_finsetInf'
- Filter.Tendsto.finset_inf_nhds
- ContinuousInf.measurableInf
- Continuous.finset_inf
- ContinuousMap.inf_apply
- ContinuousAt.inf
- MeasureTheory.AEStronglyMeasurable.fun_inf
- Continuous.finset_inf_apply
- CompactlySupportedContinuousMap.instInf
- MeasureTheory.AEEqFun.inf_le_right
- ContinuousOn.finset_inf_apply
- CompactlySupportedContinuousMap.semilatticeInf
- MeasureTheory.AEEqFun.instInf
- ContinuousOn.finset_inf'
- CompactlySupportedContinuousMap.inf_apply
- ContinuousInf.measurableInf₂
- ContinuousMap.coe_inf
- CompactlySupportedContinuousMap.coe_inf
- Continuous.inf'
- ContinuousWithinAt.inf
- MeasureTheory.AEFinStronglyMeasurable.inf
- Filter.Tendsto.finset_inf'_nhds
- ContinuousMap.inf
- Continuous.finset_inf'_apply
- Continuous.finset_inf'
Ancestors0
No ancestors.