continuousOn_iUnion — Mathlib

English

If f is locally finite, each f_i is closed, and g is continuous on each f_i, then g is continuous on the union.

Русский

Если f локально конечна, все f_i замкнуты, и g непрерывна на каждом f_i, то g непрерывна на объединении.

LaTeX

$$LocallyFinite f → (∀ i, IsClosed (f i)) → (∀ i, ContinuousOn g (f i)) → ContinuousOn g (⋃ i, f i)$$

Lean4

theorem continuousOn_iUnion {g : X → Y} (hf : LocallyFinite f) (h_cl : ∀ i, IsClosed (f i))
    (h_cont : ∀ i, ContinuousOn g (f i)) : ContinuousOn g (⋃ i, f i) :=
  hf.continuousOn_iUnion' fun i x hx ↦ h_cont i x <| (h_cl i).closure_subset hx

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