English
Let E be a normed space over a field 𝕜, and let v ∈ E with ∥v∥ = 1. The one-dimensional subspace spanned by v is canonically identified with 𝕜 via scalar multiplication, and the canonical isometry from 𝕜 into span{v} coincides with the map sending a scalar t to t·v.
Русский
Пусть E — нормированное пространство над полем 𝕜 и возьмём фиксированное v ∈ E с ∥v∥ = 1. Одномерное подсправление, порождаемое v, естественным образом канонически изоморфировано с 𝕜 через умножение на скаляр; каноническое отображение из 𝕜 в span{v} совпадает с отображением t ↦ t·v.
LaTeX
$$$ (\\text{LinearIsometry}.toSpanSingleton \\, 𝕜 \\, E \\, hv).toLinearMap = \\text{LinearMap.toSpanSingleton} \\, 𝕜 \\, E \\, v $$$
Lean4
@[simp]
theorem _root_.LinearIsometry.coe_toSpanSingleton {v : E} (hv : ‖v‖ = 1) :
(LinearIsometry.toSpanSingleton 𝕜 E hv).toLinearMap = LinearMap.toSpanSingleton 𝕜 E v :=
rfl
