ProbabilityTheory.measure_eq_zero_or_one_or_top_of_indepSet_self

∀ {Ω : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : Set Ω},
  ProbabilityTheory.IndepSet t t μ → μ t = 0 ∨ μ t = 1 ∨ μ t = ⊤

Defined in: Mathlib.Probability.Independence.ZeroOne
Cited by: 0 results in Mathlib
Foundations: Depth 180 from the axioms · uses propext, Classical.choice, Quot.sound

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Setstatement and proof · cited by 53,352
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
ENNRealstatement · cited by 9,879
Top.topstatement and proof · cited by 9,680
Filter.Eventuallyproof · cited by 3,134
ProbabilityTheory.Kernel.constproof · cited by 93
MeasureTheory.ae_dirac_eqproof · cited by 31
ProbabilityTheory.IndepSetstatement and proof · cited by 13
ProbabilityTheory.Kernel.measure_eq_zero_or_one_or_top_of_indepSet_selfproof · cited by 2

Results whose statement or proof uses this declaration.

Nothing cites this yet.