mdifferentiable_of_mdifferentiableOn_union_of_isOpen

English

If s and t are open, then MDifferentiableOn on s ∪ t is equivalent to differentiability on s and t separately.

Русский

Если s и t открыты, MDifferentiableOn на 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

theorem mdifferentiable_of_mdifferentiableOn_union_of_isOpen (hf : MDifferentiableOn I I' f s)
    (hf' : MDifferentiableOn I I' f t) (hst : s ∪ t = univ) (hs : IsOpen s) (ht : IsOpen t) : MDifferentiable I I' f :=
  by
  rw [← mdifferentiableOn_univ, ← hst]
  exact hf.union_of_isOpen hf' hs ht

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