continuous — Mathlib

English

Taking closures of a locally finite family preserves local finiteness.

Русский

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

LaTeX

$$LocallyFinite f → LocallyFinite (λ i, closure (f i))$$

Lean4

protected theorem continuous {g : X → Y} (hf : LocallyFinite f) (h_cov : ⋃ i, f i = univ) (h_cl : ∀ i, IsClosed (f i))
    (h_cont : ∀ i, ContinuousOn g (f i)) : Continuous g :=
  continuousOn_univ.1 <| h_cov ▸ hf.continuousOn_iUnion h_cl h_cont

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