generateFrom_singleton — Mathlib

English

The σ-algebra generated by a single set s is the comap of the indicator map of s to the top σ-algebra.

Русский

Сигма-алгебра, порождаемая одним множеством s, равна отображению-обратному к индикатору s от верхней σ-алгебры.

LaTeX

$$$generateFrom\\{ s \\} = MeasurableSpace.comap (\\\\cdot \\\\in s) \\\\top$$$

Lean4

/-- The sigma-algebra generated by a single set `s` is `{∅, s, sᶜ, univ}`. -/
@[simp]
theorem generateFrom_singleton (s : Set α) : generateFrom { s } = MeasurableSpace.comap (· ∈ s) ⊤ := by
  classical
  letI : MeasurableSpace α := generateFrom { s }
  refine le_antisymm (generateFrom_le fun t ht => ⟨{ True }, trivial, by simp [ht.symm]⟩) ?_
  rintro _ ⟨u, -, rfl⟩
  exact (show MeasurableSet s from GenerateMeasurable.basic _ <| mem_singleton s).mem trivial

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