English
If a family of open sets s_i cover a union, then ContDiffOn 𝕜 n f on the union is equivalent to ContDiffOn 𝕜 n f on every s_i.
Русский
Если множество s_i образует покрытие объединения, то ContDiffOn 𝕜 n f на объединении эквивалентно ContDiffOn 𝕜 n f на каждом s_i.
LaTeX
$$$ \operatorname{ContDiffOn}_{\mathbb{K}}^{n} f (\bigcup_i s_i) \iff \forall i, \operatorname{ContDiffOn}_{\mathbb{K}}^{n} f (s_i) $$$
Lean4
/-- If a function is `C^k` on open sets `s i`, it is `C^k` on their union -/
theorem iUnion_of_isOpen {ι : Type*} {s : ι → Set E} (hf : ∀ i : ι, ContDiffOn 𝕜 n f (s i)) (hs : ∀ i, IsOpen (s i)) :
ContDiffOn 𝕜 n f (⋃ i, s i) := by
rintro x ⟨si, ⟨i, rfl⟩, hxsi⟩
exact (hf i).contDiffAt ((hs i).mem_nhds hxsi) |>.contDiffWithinAt
