closure_iUnion — Mathlib

English

A set-theoretic simplification of closure of unions under local finiteness.

Русский

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

LaTeX

$$LocallyFinite f → (closure_iUnion ... )$$

Lean4

theorem closure_iUnion (h : LocallyFinite f) : closure (⋃ i, f i) = ⋃ i, closure (f i) :=
  by
  ext x
  simp only [mem_closure_iff_nhdsWithin_neBot, h.nhdsWithin_iUnion, iSup_neBot, mem_iUnion]

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