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) _