Theorems · Inductive type · measure theory
MeasureTheory.IsZeroOneMeasure
{α : Type u_1} → {mα : MeasurableSpace α} → MeasureTheory.Measure α → PropA measure is a zero-one measure if it only takes the values 0 or 1.
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MeasurableSpacestatement · cited by 13,106
- MeasureTheory.Measurestatement · cited by 10,939
Cited by10
Results whose statement or proof uses this declaration.
- MeasureTheory.Measure.zero_onestatement and proof · cited by 5
- MeasureTheory.IsZeroOneMeasure.measure_univstatement and proof · cited by 2
- MeasureTheory.IsZeroOneMeasure.exists_eq_diracstatement and proof · cited by 1
- MeasureTheory.IsZeroOneMeasure.exists_measure_eq_one_iff_measure_univ_eq_onestatement and proof · cited by 1
- MeasureTheory.IsZeroOneMeasure.measure_inter_eq_onestatement and proof · cited by 1
- MeasureTheory.IsZeroOneMeasure.measure_inter_eq_prodstatement and proof · cited by 1
- MeasureTheory.IsZeroOneMeasure.zero_one₀statement and proof · cited by 1
- ProbabilityTheory.Kernel.isDeterministic_iff_isZeroOneMeasurestatement and proof · cited by 0
- MeasureTheory.IsZeroOneMeasure.casesOnstatement and proof · cited by 0
- MeasureTheory.IsZeroOneMeasure.recOnstatement and proof · cited by 0