union_of_isOpen — Mathlib

English

If f has Frechet derivative at x₀, then (f x − f x₀) = O(x − x₀) in nhds around x₀.

Русский

Если у f в x₀ есть производная Фреше, то f(x)−f(x₀) = O(x−x₀) в окрестности x₀.

LaTeX

$$HasFDerivAt f f' x₀ → Asymptotics.IsBigO (nhds x₀) (fun x => f x - f x₀) (fun x => x - x₀)$$

Lean4

/-- If a function is differentiable on two open sets, it is also differentiable on their union. -/
theorem union_of_isOpen (hf : DifferentiableOn 𝕜 f s) (hf' : DifferentiableOn 𝕜 f t) (hs : IsOpen s) (ht : IsOpen t) :
    DifferentiableOn 𝕜 f (s ∪ t) := by
  intro x hx
  obtain (hx | hx) := hx
  · exact (hf x hx).differentiableAt (hs.mem_nhds hx) |>.differentiableWithinAt
  · exact (hf' x hx).differentiableAt (ht.mem_nhds hx) |>.differentiableWithinAt

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