English
If a function is continuous on each set in a family of open sets whose union is the whole space, then it is continuous on the entire space.
Русский
Если функция непрерывна на каждом множестве семейства открытых множеств, чья объединение равно всей области, тогда она непрерывна на всей области.
LaTeX
$$$\\forall i,\\; \\text{ContinuousOn } f (s_i) \\Rightarrow \\text{ContinuousOn } f (\\bigcup_i s_i)$ with appropriate hypotheses on openness$$
Lean4
/-- If a function is continuous on open sets `s i`, it is continuous on their union -/
theorem iUnion_of_isOpen {ι : Type*} {s : ι → Set α} (hf : ∀ i : ι, ContinuousOn f (s i)) (hs : ∀ i, IsOpen (s i)) :
ContinuousOn f (⋃ i, s i) := by
rintro x ⟨si, ⟨i, rfl⟩, hxsi⟩
exact (hf i).continuousAt ((hs i).mem_nhds hxsi) |>.continuousWithinAt
