Structures · Analysis
MeasurableSpace.SeparatesPoints
We say that a measurable space separates points if for any two distinct points, there is a measurable set containing one but not the other.
- Shape
- One type argument · adds separates
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- Set.Elem
How is a type an instance?
Loading the hierarchy index…
Assumed by17
- MeasurableSpace.SeparatesPoints.separates
- MeasurableSpace.separatesPoints_def
- MeasurableSpace.injective_mapNatBool
- MeasurableSpace.exists_measurableSet_of_ne
- MeasurableSpace.measurableEquiv_nat_bool_of_countablyGenerated
- MeasureTheory.dirac_eq_dirac_iff
- MeasureTheory.dirac_ne_dirac
- MeasurableSpace.separating_of_generateFrom
- MeasureTheory.injective_diracProba
- eq_const_of_measurable_bot
- exists_borelSpace_of_countablyGenerated_of_separatesPoints
- MeasureTheory.dirac_ne_dirac_iff
- MeasurableSpace.Subtype.separatesPoints
- MeasurableSpace.MeasurableSingletonClass.of_separatesPoints
- MeasureTheory.injective_dirac
- MeasurableSpace.countablySeparated_of_separatesPoints
- MeasurableSpace.SeparatesPoints.mono
Ancestors0
No ancestors.