contDiffOn_union_iff_of_isOpen — Mathlib

English

Let s and t be open. Then ContDiffOn 𝕜 n f (s ∪ t) is equivalent to ContDiffOn 𝕜 n f s and ContDiffOn 𝕜 n f t.

Русский

Пусть s и t открыты. Тогда ContDiffOn 𝕜 n f (s ∪ t) эквивалентно ContDiffOn 𝕜 n f s и ContDiffOn 𝕜 n f t.

LaTeX

$$$ \operatorname{ContDiffOn}_{\mathbb{K}}^{n} f (s \cup t) \iff \operatorname{ContDiffOn}_{\mathbb{K}}^{n} f s \land \operatorname{ContDiffOn}_{\mathbb{K}}^{n} f t $$$

Lean4

/-- A function is `C^k` on two open sets iff it is `C^k` on their union. -/
theorem contDiffOn_union_iff_of_isOpen (hs : IsOpen s) (ht : IsOpen t) :
    ContDiffOn 𝕜 n f (s ∪ t) ↔ ContDiffOn 𝕜 n f s ∧ ContDiffOn 𝕜 n f t :=
  ⟨fun h ↦ ⟨h.mono subset_union_left, h.mono subset_union_right⟩, fun ⟨hfs, hft⟩ ↦
    ContDiffOn.union_of_isOpen hfs hft hs ht⟩

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