differentiableOn_of_locally_differentiableOn

English

If t is a neighborhood of x, then differentiability within s ∩ t at x is equivalent to differentiability within s at x.

Русский

Если t является окрестностью x, то дифференцируемость внутри s ∩ t в x эквивалентна дифференцируемости внутри s в x.

LaTeX

$$$\bigl( t \in 𝓝 x \bigr) \Rightarrow \mathrm{DifferentiableWithinAt } 𝕜 f (s \cap t) x \iff \mathrm{DifferentiableWithinAt } 𝕜 f s x$$$

Lean4

theorem differentiableOn_of_locally_differentiableOn
    (h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ DifferentiableOn 𝕜 f (s ∩ u)) : DifferentiableOn 𝕜 f s :=
  by
  intro x xs
  rcases h x xs with ⟨t, t_open, xt, ht⟩
  exact (differentiableWithinAt_inter (IsOpen.mem_nhds t_open xt)).1 (ht x ⟨xs, xt⟩)

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