isClosed_iUnion — Mathlib

English

Additional simplifications for closure of iUnion under locally finite families.

Русский

Дополнительные упрощения для замыкания объединения при локально конечной семействах.

LaTeX

$$LocallyFinite f → closure (⋃ i, f i) = ⋃ i, closure (f i)$$

Lean4

theorem isClosed_iUnion (hf : LocallyFinite f) (hc : ∀ i, IsClosed (f i)) : IsClosed (⋃ i, f i) := by
  simp only [← closure_eq_iff_isClosed, hf.closure_iUnion, (hc _).closure_eq]

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