coord_norm — Mathlib

English

For x ≠ 0 and a nonzero field 𝕜, the norm of the coordinate map satisfies ||coord_𝕜 x h|| = ||x||^{-1}.

Русский

Для x ≠ 0 и поля 𝕜 выполняется: ||coord_𝕜 x h|| = ||x||^{-1}.

LaTeX

$$$$\\|\\mathrm{coord}_{\\,\\mathbb{K}}(x,h)\\| = \\|x\\|^{-1}.$$$$

Lean4

@[simp]
theorem coord_norm (x : E) (h : x ≠ 0) : ‖coord 𝕜 x h‖ = ‖x‖⁻¹ :=
  by
  have hx : 0 < ‖x‖ := norm_pos_iff.mpr h
  haveI : Nontrivial (𝕜 ∙ x) := Submodule.nontrivial_span_singleton h
  exact
    ContinuousLinearMap.homothety_norm _ fun y =>
      homothety_inverse _ hx _ (LinearEquiv.toSpanNonzeroSingleton_homothety 𝕜 x h) _

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