generateFrom_singleton_le — Mathlib

English

If s is measurable, then generateFrom {s} is contained in any larger σ-algebra m.

Русский

Если s измеримо, то порождение {s} должно быть включено в любую большую σ-алгебру m.

LaTeX

$$$\\\\forall {m : MeasurableSpace α} {s : Set α}, MeasurableSet s \\\\Rightarrow MeasurableSpace.generateFrom \\\\{ s \\\} \\\\le m$$$

Lean4

theorem generateFrom_singleton_le {m : MeasurableSpace α} {s : Set α} (hs : MeasurableSet s) :
    MeasurableSpace.generateFrom { s } ≤ m :=
  generateFrom_le (fun _ ht ↦ mem_singleton_iff.1 ht ▸ hs)

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