Structures · Analysis
MeasurableSpace.CountablySeparated
We say that a measurable space is countably separated if there is a countable sequence of measurable sets separating points.
- Shape
- One type argument · adds countably_separated
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 by21
- Measurable.map_measurableSpace_eq
- Measurable.measurableSet_preimage_iff_of_surjective
- QuasiErgodic.ae_eq_const_of_ae_eq_comp_of_ae_range₀
- exists_opensMeasurableSpace_of_countablySeparated
- MeasurableSpace.exists_countablyGenerated_le_of_countablySeparated
- Measurable.measurableSet_preimage_iff_preimage_val
- MeasurableSpace.measurable_injection_nat_bool_of_countablySeparated
- Ergodic.ae_eq_const_of_ae_eq_comp₀
- QuasiErgodic.ae_eq_const_of_ae_eq_comp₀
- MeasurableSpace.CountablySeparated.countably_separated
- MeasurableSet.image_of_measurable_injOn
- MeasurableSpace.Subtype.countablySeparated
- Measurable.measurableEmbedding
- MeasurableSpace.hasCountableSeparatingOn_of_countablySeparated_subtype
- Measurable.measurableSet_preimage_iff_inter_range
- MeasurableSpace.hasCountableSeparatingOn_of_countablySeparated
- Measurable.measurable_comp_iff_of_surjective
- PreErgodic.ae_eq_const_of_ae_eq_comp
- Measurable.measurable_comp_iff_restrict
- MeasurableSpace.CountablySeparated.mono
- MeasurableSpace.measurableSingletonClass_of_countablySeparated
Ancestors0
No ancestors.