Theorems · Theorem · measure theory

MeasurableSpace.disjoint_countablePartition

∀ {α : Type u_1} [m : MeasurableSpace α] [h : MeasurableSpace.CountablyGenerated α] {n : ℕ} {s t : Set α},
  s ∈ MeasurableSpace.countablePartition α n → t ∈ MeasurableSpace.countablePartition α n → s ≠ t → Disjoint s t

Defined in

Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Cited by

2 results in Mathlib

Foundations

Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceMeasurableSpace.CountablyGenerated