iUnion_mem_generateMeasurableRec — Mathlib

English

The union over n of f(n) belongs to generateMeasurableRec s i under appropriate assumptions.

Русский

Объединение по n функций f(n) принадлежит generateMeasurableRec s i при заданных предпосылках.

LaTeX

$$$\\bigcup_{n} f(n) \\in generateMeasurableRec(s,i)$$$

Lean4

theorem iUnion_mem_generateMeasurableRec {s : Set (Set α)} {i : Ordinal} {f : ℕ → Set α}
    (hf : ∀ n, ∃ j < i, f n ∈ generateMeasurableRec s j) : ⋃ n, f n ∈ generateMeasurableRec s i :=
  by
  unfold generateMeasurableRec
  exact
    mem_union_right _
      ⟨fun n =>
        ⟨f n,
          let ⟨j, hj, hf⟩ := hf n;
          mem_iUnion₂.2 ⟨j, hj, hf⟩⟩,
        rfl⟩

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