isCountablySpanning_measurableSet

English

The collection of measurable sets is countably spanning.

Русский

Множество измеримых множеств счётно образуют полное пространство.

LaTeX

$$$\\text{IsCountablySpanning}\\{s : {\\text{Set } \\alpha \\mid \\text{MeasurableSet } s}\\}$$$

Lean4

theorem isCountablySpanning_measurableSet [MeasurableSpace α] : IsCountablySpanning {s : Set α | MeasurableSet s} :=
  ⟨fun _ => univ, fun _ => MeasurableSet.univ, iUnion_const _⟩

Похожие утверждения