compl_mem_generateMeasurableRec — Mathlib

English

If j < i and t ∈ generateMeasurableRec s j, then t^c ∈ generateMeasurableRec s i.

Русский

Если j<i и t ∈ generateMeasurableRec s j, то t^c ∈ generateMeasurableRec s i.

LaTeX

$$$j

Lean4

theorem compl_mem_generateMeasurableRec {s : Set (Set α)} {i j : Ordinal} (h : j < i) {t : Set α} (ht : t ∈ generateMeasurableRec s j) : tᶜ ∈ generateMeasurableRec s i := by unfold generateMeasurableRec exact mem_union_left _ (mem_union_right _ ⟨t, mem_iUnion₂.2 ⟨j, h, ht⟩, rfl⟩)

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