closure — Mathlib

English

The closure of the union equals the union of closures for a locally finite family.

Русский

Замыкание объединения равно объединению замыканий для локально конечной семейства.

LaTeX

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

Lean4

protected theorem closure (hf : LocallyFinite f) : LocallyFinite fun i => closure (f i) :=
  by
  intro x
  rcases hf x with ⟨s, hsx, hsf⟩
  refine ⟨interior s, interior_mem_nhds.2 hsx, hsf.subset fun i hi => ?_⟩
  exact (hi.mono isOpen_interior.closure_inter).of_closure.mono (inter_subset_inter_right _ interior_subset)

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