English
If hf and hf' are ContDiffOn on two open sets whose union is the whole space, then f is ContDiff on the whole space.
Русский
Если hf и hf' заданы на двух открытых множествах, чьи объединение равно всё пространство, то f — ContDiff на всем пространстве.
LaTeX
$$$ \operatorname{ContDiffOn}_{\mathbb{K}}^{n} f (s) \land \operatorname{ContDiffOn}_{\mathbb{K}}^{n} f (t) \land s \cup t = \mathrm{univ} \Rightarrow \operatorname{ContDiff}_{\mathbb{K}}^{n} f$$$
Lean4
/-- A function is `C^k` on a union of open sets `s i` iff it is `C^k` on each `s i`. -/
theorem contDiffOn_iUnion_iff_of_isOpen {ι : Type*} {s : ι → Set E} (hs : ∀ i, IsOpen (s i)) :
ContDiffOn 𝕜 n f (⋃ i, s i) ↔ ∀ i : ι, ContDiffOn 𝕜 n f (s i) :=
⟨fun h i ↦ h.mono <| subset_iUnion_of_subset i fun _ a ↦ a, fun h ↦ ContDiffOn.iUnion_of_isOpen h hs⟩
