continuousOn_iUnion' — Mathlib

English

If each f_i is a domain on which g is continuous within the closure of f_i, then g is continuous on the union.

Русский

Если для каждого i функция g непрерывна внутри замыкания f_i, тогда она непрерывна на объединении f_i.

LaTeX

$$LocallyFinite f → (∀ i, x, x ∈ closure (f i) → ContinuousWithinAt g (f i) x) → ContinuousOn g (⋃ i, f i)$$

Lean4

theorem continuousOn_iUnion' {g : X → Y} (hf : LocallyFinite f)
    (hc : ∀ i x, x ∈ closure (f i) → ContinuousWithinAt g (f i) x) : ContinuousOn g (⋃ i, f i) :=
  by
  rintro x -
  rw [ContinuousWithinAt, hf.nhdsWithin_iUnion, tendsto_iSup]
  intro i
  by_cases hx : x ∈ closure (f i)
  · exact hc i _ hx
  · rw [mem_closure_iff_nhdsWithin_neBot, not_neBot] at hx
    rw [hx]
    exact tendsto_bot

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