mdifferentiableWithinAt_insert_self

English

Let f be a map between manifolds and x ∈ M. For any subset s ⊆ M, f is differentiable within at x on s if and only if f is differentiable within at x on the set obtained by inserting x into s.

Русский

Пусть f: M → M' и x ∈ M. Для любого подмножества s ⊆ M функция f дифференцируема внутри x на s тогда и только тогда, когда она дифференцируема внутри x на множество, полученное добавлением x к s.

LaTeX

$$$$MDifferentiableWithinAt I I' f (insert x s) x \\iff MDifferentiableWithinAt I I' f s x$$$$

Lean4

theorem mdifferentiableWithinAt_insert_self :
    MDifferentiableWithinAt I I' f (insert x s) x ↔ MDifferentiableWithinAt I I' f s x :=
  ⟨fun h ↦ h.mono (subset_insert x s), fun h ↦ h.hasMFDerivWithinAt.insert.mdifferentiableWithinAt⟩

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