contDiff_of_contDiffOn_iUnion_of_isOpen

English

Let hf_i be ContDiffOn 𝕜 n f on s_i for all i and all s_i be open; then f is ContDiff 𝕜 n on the union of all s_i when the index set is arbitrary.

Русский

Пусть для каждого i функция f задана как ContDiffOn 𝕜 n f на s_i, где s_i открыты; тогда f ∈ ContDiff 𝕜 n на объединении s_i.

LaTeX

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

Lean4

theorem contDiff_of_contDiffOn_iUnion_of_isOpen {ι : Type*} {s : ι → Set E} (hf : ∀ i : ι, ContDiffOn 𝕜 n f (s i))
    (hs : ∀ i, IsOpen (s i)) (hs' : ⋃ i, s i = univ) : ContDiff 𝕜 n f :=
  by
  rw [← contDiffOn_univ, ← hs']
  exact ContDiffOn.iUnion_of_isOpen hf hs

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