norm_tangentSpace_vectorSpace — Mathlib

English

The norm on the tangent space at x agrees with the norm of the corresponding vector under the canonical identification T_xF ≅ F.

Русский

Норма на касательном пространстве в точке x совпадает с нормой соответствующего вектора под канонической идентификацией T_xF ≅ F.

LaTeX

$$$$\\|v\\| = \\|V\\|\\quad\\text{where }V\\text{ is the image of }v\\text{ under the natural identification }T_xF \\cong F.$$$$

Lean4

theorem norm_tangentSpace_vectorSpace {x : F} {v : TangentSpace 𝓘(ℝ, F) x} :
    ‖v‖ =
      ‖letI V : F := v;
        V‖ :=
  by rw [norm_eq_sqrt_real_inner, norm_eq_sqrt_real_inner]

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