generateFrom_measurableSet — Mathlib

English

For any measurable space α, generateFrom of the family {s : Set α | MeasurableSet s} equals the given space.

Русский

Для любого множества α порожденное GenerateFrom по семейству {s | MeasurableSet s} равно данной структуре пространства измеримости.

LaTeX

$$$\\text{generateFrom}(\\{s : Set\\alpha \\mid MeasurableSet s\\}) = \\text{the given MeasurableSpace on } \\alpha$$$

Lean4

@[simp]
theorem generateFrom_measurableSet [MeasurableSpace α] : generateFrom {s : Set α | MeasurableSet s} = ‹_› :=
  le_antisymm (generateFrom_le fun _ => id) fun _ => measurableSet_generateFrom

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