union_of_isOpen — Mathlib

English

If f is C^n on s and on t, and s,t are open, then f is C^n on s ∪ t.

Русский

Если функция C^n на s и на t, и s,t открыты, то она C^n на их объединении.

LaTeX

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

Lean4

/-- If a function is `C^k` on two open sets, it is also `C^n` on their union. -/
theorem union_of_isOpen (hf : ContDiffOn 𝕜 n f s) (hf' : ContDiffOn 𝕜 n f t) (hs : IsOpen s) (ht : IsOpen t) :
    ContDiffOn 𝕜 n f (s ∪ t) := by
  rintro x (hx | hx)
  · exact (hf x hx).contDiffAt (hs.mem_nhds hx) |>.contDiffWithinAt
  · exact (hf' x hx).contDiffAt (ht.mem_nhds hx) |>.contDiffWithinAt

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