dense_differentiableAt_norm — Mathlib

English

In a real finite-dimensional space, the set where the norm is differentiable is dense.

Русский

В вещественном конечномерном пространстве множество точек, где норма дифференцируема, густо.

LaTeX

$$$\\text{dense\\_differentiableAt}$$$

Lean4

/-- In a real finite-dimensional normed vector space,
  the set of points where the norm is differentiable at is dense. -/
theorem dense_differentiableAt_norm : Dense {x : E | DifferentiableAt ℝ (‖·‖) x} :=
  let _ : MeasurableSpace E := borel E
  have _ : BorelSpace E := ⟨rfl⟩
  let w := Basis.ofVectorSpace ℝ E
  MeasureTheory.Measure.dense_of_ae (ae_differentiableAt_norm (μ := w.addHaar))

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