Structures · Analysis
MeasurableSup₂
We say that a type has MeasurableSup₂ if uncurry (· ⊔ ·) is a measurable functions.
For a typeclass assuming measurability of (c ⊔ ·) and (· ⊔ c) see MeasurableSup.
- Defined in
- Mathlib.MeasureTheory.Order.Lattice
- Shape
- One type argument · adds measurable_sup
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- OrderDual
How is a type an instance?
Loading the hierarchy index…
Assumed by18
- Measurable.sup
- measurable_abs
- MeasurableSup₂.measurable_sup
- Finset.measurable_range_sup''
- measurable_mabs
- AEMeasurable.sup
- Finset.measurable_range_sup'
- Finset.measurable_sup'
- OrderDual.instMeasurableInf₂
- AEMeasurable.sup'
- Measurable.fun_sup
- MeasurableSup₂.toMeasurableSup
- AEMeasurable.mabs
- Measurable.abs
- Measurable.mabs
- AEMeasurable.fun_sup
- Measurable.sup'
- AEMeasurable.abs
Ancestors0
No ancestors.