differentiableWithinAt — Mathlib

English

Let iso: E ≃L[𝕜] F. Then iso is differentiable within s at x: DifferentiableWithinAt 𝕜 iso s x.

Русский

Пусть iso: E ≃L[𝕜] F. Тогда iso дифференцируема внутри s в точке x: DifferentiableWithinAt 𝕜 iso s x.

LaTeX

$$$\text{DifferentiableWithinAt}_{𝕜}(iso, s, x)$$$

Lean4

@[fun_prop]
protected theorem differentiableWithinAt : DifferentiableWithinAt 𝕜 iso s x :=
  iso.differentiableAt.differentiableWithinAt

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