generateFrom_le — Mathlib

English

If s ⊆ t are collections of subsets, then generateFrom s ≤ generateFrom t.

Русский

Если s ⊆ t — коллекции подмножеств, то порожденная сигма-алгебра GenerateFrom s меньше или равна GenerateFrom t.

LaTeX

$$$s \\subseteq t \\implies GenerateFrom(s) \\le GenerateFrom(t)$$$

Lean4

theorem generateFrom_le {s : Set (Set α)} {m : MeasurableSpace α} (h : ∀ t ∈ s, MeasurableSet[m] t) :
    generateFrom s ≤ m := fun t (ht : GenerateMeasurable s t) =>
  ht.recOn h .empty (fun _ _ => .compl) fun _ _ hf => .iUnion hf

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