generateMeasurableRec_subset — Mathlib

English

For any i, generateMeasurableRec s i is a subset of the set of t that are generated by s.

Русский

Для любого i множество generateMeasurableRec(s,i) является подмножеством множества t, порождаемого s.

LaTeX

$$$\\mathrm{generateMeasurableRec}(s,i) \\subseteq \\{ t \\mid \\mathrm{GenerateMeasurable}(s,t) \\}$$$

Lean4

theorem generateMeasurableRec_subset (s : Set (Set α)) (i : Ordinal) :
    generateMeasurableRec s i ⊆ {t | GenerateMeasurable s t} :=
  by
  apply WellFoundedLT.induction i
  exact fun i IH t ht =>
    generateMeasurableRec_induction .basic .empty (fun u _ ⟨j, hj, hj'⟩ => .compl _ (IH j hj hj'))
      (fun f H => .iUnion _ fun n => (H n).1) ht

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