mdifferentiableOn_of_locally_mdifferentiableOn

English

If for every x in s there exists an open set u with x ∈ u and f is differentiable on s ∩ u, then f is differentiable on s.

Русский

Если для каждого x ∈ s существует открытое множество u с x ∈ u и f дифференцируема на s ∩ u, то f дифференцируема на s.

LaTeX

$$(∀ x ∈ s, ∃ u Open, x ∈ u ∧ MDifferentiableOn I I' f (s ∩ u)) → MDifferentiableOn I I' f s$$

Lean4

theorem mdifferentiableOn_of_locally_mdifferentiableOn
    (h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ MDifferentiableOn I I' f (s ∩ u)) : MDifferentiableOn I I' f s :=
  by
  intro x xs
  rcases h x xs with ⟨t, t_open, xt, ht⟩
  exact (mdifferentiableWithinAt_inter (t_open.mem_nhds xt)).1 (ht x ⟨xs, xt⟩)

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