English
A function is differentiable on the union of a family of open sets if and only if it is differentiable on every member of the family.
Русский
Функция дифференцируема на объединении семейства открытых множеств тогда и только тогда, когда она дифференцируема на каждом элементе семейства.
LaTeX
$$$$IsOpen\\(s_i\\) \\text{ for all } i \\Rightarrow (MDifferentiableOn I I' f (\\bigcup_i s_i) \\iff \\forall i, MDifferentiableOn I I' f (s_i))$$$$
Lean4
/-- If a function is differentiable on open sets `s i`, it is differentiable on their union. -/
theorem iUnion_of_isOpen {ι : Type*} {s : ι → Set M} (hf : ∀ i : ι, MDifferentiableOn I I' f (s i))
(hs : ∀ i, IsOpen (s i)) : MDifferentiableOn I I' f (⋃ i, s i) :=
by
rintro x ⟨si, ⟨i, rfl⟩, hxsi⟩
exact (hf i).mdifferentiableAt ((hs i).mem_nhds hxsi) |>.mdifferentiableWithinAt
