continuous' — Mathlib

English

If union equals the whole space and each f_i is closed, and g is continuous on each f_i, then g is continuous on the whole space.

Русский

Если объединение покрывает всю X, каждое f_i замкнуто, и g непрерывна на каждом f_i, тогда g непрерывна на всей X.

LaTeX

$$LocallyFinite f → Eq (⋃ i, f i) Set.univ → (∀ i, IsClosed (f i)) → (∀ i, ContinuousOn g (f i)) → Continuous g$$

Lean4

protected theorem continuous' {g : X → Y} (hf : LocallyFinite f) (h_cov : ⋃ i, f i = univ)
    (hc : ∀ i x, x ∈ closure (f i) → ContinuousWithinAt g (f i) x) : Continuous g :=
  continuousOn_univ.1 <| h_cov ▸ hf.continuousOn_iUnion' hc

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