English
If a function is differentiable on two open sets s and t, then it is differentiable on their union.
Русский
Если функция дифференцируема на двух открытых множествах s и t, то она дифференцируема на их объединении.
LaTeX
$$$$MDifferentiableOn I I' f s \\rightarrow MDifferentiableOn I I' f t \\rightarrow IsOpen s \\rightarrow IsOpen t \\rightarrow MDifferentiableOn I I' f (s \\cup t)$$$$
Lean4
/-- If a function is differentiable on two open sets, it is also differentiable on their union. -/
theorem union_of_isOpen (hf : MDifferentiableOn I I' f s) (hf' : MDifferentiableOn I I' f t) (hs : IsOpen s)
(ht : IsOpen t) : MDifferentiableOn I I' f (s ∪ t) :=
by
intro x hx
obtain (hx | hx) := hx
· exact (hf x hx).mdifferentiableAt (hs.mem_nhds hx) |>.mdifferentiableWithinAt
· exact (hf' x hx).mdifferentiableAt (ht.mem_nhds hx) |>.mdifferentiableWithinAt
