contDiff_of_contDiffOn_union_of_isOpen

English

For any index set, if each s_i is open and f is C^n on each s_i, then f is C^n on the union.

Русский

Для произвольного множества индексов, если каждое s_i открыто и f — C^n на каждом s_i, то f — C^n на объединение.

LaTeX

$$$ \forall i,\operatorname{IsOpen}(s_i) \Rightarrow \operatorname{ContDiffOn}_{\mathbb{K}}^{n} f (\bigcup_i s_i) \iff \forall i, \operatorname{ContDiffOn}_{\mathbb{K}}^{n} f (s_i)$$$

Lean4

theorem contDiff_of_contDiffOn_union_of_isOpen (hf : ContDiffOn 𝕜 n f s) (hf' : ContDiffOn 𝕜 n f t) (hst : s ∪ t = univ)
    (hs : IsOpen s) (ht : IsOpen t) : ContDiff 𝕜 n f :=
  by
  rw [← contDiffOn_univ, ← hst]
  exact hf.union_of_isOpen hf' hs ht

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