differentiableOn_union_iff_of_isOpen

English

If f is differentiable on two open sets s and t, then f is differentiable on their union.

Русский

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

LaTeX

$$DifferentiableOn 𝕜 f s → DifferentiableOn 𝕜 f t → IsOpen s → IsOpen t → DifferentiableOn 𝕜 f (s ∪ t)$$

Lean4

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

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