English
Let 𝕜 be a normed division ring. The map that sends a point on the unit sphere to its corresponding unit in 𝕜 is injective. In particular, if x and y are points with ‖x‖ = ‖y‖ = 1 and unitSphereToUnits 𝕜 x = unitSphereToUnits 𝕜 y, then x = y.
Русский
Пусть 𝕜 — нормированное делимое кольцо. Отображение, отправляющее точку на единичной сфере в соответствующую единицу в 𝕜, инъективно. То есть если x,y ∈ sphere(0,1) и unitSphereToUnits 𝕜 x = unitSphereToUnits 𝕜 y, то x = y.
LaTeX
$$$\\forall x,y \\in \\mathrm{sphere}(0,1),\\; \\mathrm{unitSphereToUnits}(\\,\\mathbb{K}\\,)(x) = \\mathrm{unitSphereToUnits}(\\,\\mathbb{K}\\,)(y) \\Rightarrow x = y$$$
Lean4
theorem unitSphereToUnits_injective [NormedDivisionRing 𝕜] : Function.Injective (unitSphereToUnits 𝕜) := fun x y h =>
Subtype.eq <| by convert congr_arg Units.val h
