coord — Mathlib

English

The coord map is the inverse of the span map: coord 𝕜 x h is the inverse of the isomorphism 𝕜 ≃L[𝕜] 𝕜 ∙ x.

Русский

Координатная карта является обратной к отображению, задающему Span: coord 𝕜 x h — обратная к изоморфизму 𝕜 ≃L[𝕜] 𝕜·x.

LaTeX

$$$ coord\\, 𝕜\\, x\\, h = (toSpanNonzeroSingleton\\, 𝕜\\, x\\, h)^{-1}$$$

Lean4

/-- Given a nonzero element `x` of a normed space `E₁` over a field `𝕜`, the natural continuous
linear map from the span of `x` to `𝕜`. -/
noncomputable def coord (x : E) (h : x ≠ 0) : StrongDual 𝕜 (𝕜 ∙ x) :=
  (toSpanNonzeroSingleton 𝕜 x h).symm

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