continuous_of_cover_nhds — Mathlib

English

If a collection of sets covers every point of α by neighborhoods, and f is continuous on each piece, then f is continuous on the whole space.

Русский

Если каждая точка пространства покрывается окрестностями из покрывающей семьи, и f непрерывна на каждом фрагменте, то f непрерывна на всей области.

LaTeX

$$$\\forall x, \\exists i, s_i \\in 𝓝 x \\land ContinuousOn f (s_i) \\Rightarrow Continuous f$$$

Lean4

theorem continuous_of_cover_nhds {ι : Sort*} {s : ι → Set α} (hs : ∀ x : α, ∃ i, s i ∈ 𝓝 x)
    (hf : ∀ i, ContinuousOn f (s i)) : Continuous f :=
  continuous_iff_continuousAt.mpr fun x ↦
    let ⟨i, hi⟩ := hs x;
    by
    rw [ContinuousAt, ← nhdsWithin_eq_nhds.2 hi]
    exact hf _ _ (mem_of_mem_nhds hi)

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