nnnorm_tangentSpace_vectorSpace — Mathlib

English

The nonnegative-norm (nnnorm) on the tangent space agrees with the underlying vector-space norm under the canonical identification with F.

Русский

NNNorm-норма на касательном пространстве совпадает с нормой пространства F под канонической идентификацией.

LaTeX

$$$$\\|v\\|_+ = \\|V\\|_+ \\quad\\text{where }V\\text{ is the image of }v\\text{ in }F.$$$$

Lean4

theorem nnnorm_tangentSpace_vectorSpace {x : F} {v : TangentSpace 𝓘(ℝ, F) x} :
    ‖v‖₊ =
      ‖letI V : F := v;
        V‖₊ :=
  by simp [nnnorm, norm_tangentSpace_vectorSpace]

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