ae_differentiableAt_norm — Mathlib

English

A Lipschitz map f: E → F between finite-dimensional spaces is differentiable almost everywhere.

Русский

Липшицева отображение между конечномерными пространствами дифференцируемо почти всюду.

LaTeX

$$$\text{ae\_differentiableAt}$$$

Lean4

/-- In a real finite-dimensional normed vector space,
  the norm is almost everywhere differentiable. -/
theorem ae_differentiableAt_norm : ∀ᵐ x ∂μ, DifferentiableAt ℝ (‖·‖) x :=
  lipschitzWith_one_norm.ae_differentiableAt

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