mdifferentiableOn_union_iff_of_isOpen

English

If s and t are open, differentiability on s ∪ t is equivalent to differentiability on both s and t.

Русский

Если s и t открыты, дифференциируемость на s ∪ t эквивалентна дифференциируемости на s и на t.

LaTeX

$$$$IsOpen s \\land IsOpen t \\rightarrow (MDifferentiableOn I I' f (s \\cup t) \\iff (MDifferentiableOn I I' f s \\land MDifferentiableOn I I' f t))$$$$

Lean4

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

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