Theorems · Inductive type · measure theory
MeasurableSpace.SeparatesPoints
(α : Type u_3) → [m : MeasurableSpace α] → Prop
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.
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- MeasurableSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MeasurableSpacestatement · cited by 13,106
Cited by20
Results whose statement or proof uses this declaration.
- MeasurableSpace.SeparatesPoints.separatesstatement and proof · cited by 3
- exists_opensMeasurableSpace_of_countablySeparatedproof · cited by 2
- MeasurableSpace.injective_mapNatBoolstatement and proof · cited by 2
- MeasurableSpace.exists_countablyGenerated_le_of_countablySeparatedstatement · cited by 2
- MeasurableSpace.exists_measurableSet_of_nestatement and proof · cited by 2
- MeasurableSpace.separatesPoints_defstatement and proof · cited by 2
- MeasurableSpace.measurableEquiv_nat_bool_of_countablyGeneratedstatement and proof · cited by 1
- MeasureTheory.dirac_eq_dirac_iffstatement and proof · cited by 1
- exists_borelSpace_of_countablyGenerated_of_separatesPointsstatement and proof · cited by 1
- MeasureTheory.dirac_ne_diracstatement and proof · cited by 1
- MeasureTheory.dirac_ne_dirac_iffstatement and proof · cited by 1
- MeasurableSpace.measurable_injection_nat_bool_of_countablySeparatedproof · cited by 1