English
An alternative description of the norm on the quotient: ∥(x : M ⧸ S)∥ = infDist(x, S) where x ∈ M.
Русский
Альтернативное представление нормы на факторгруппе: ∥(x : M ⧸ S)∥ = infDist(x, S).
LaTeX
$$$\|\,(x : M ⧸ S)\,\| = \operatorname{infDist}(x, S)$$$
Lean4
/-- An alternative definition of the norm on the quotient group: the norm of `((x : M) : M ⧸ S)` is
equal to the distance from `x` to `S`. -/
@[to_additive /-- An alternative definition of the norm on the quotient group: the norm of `((x : M) : M ⧸ S)` is
equal to the distance from `x` to `S`. -/
]
theorem norm_mk (x : M) : ‖(x : M ⧸ S)‖ = infDist x S :=
by
rw [norm_eq_infDist, ← infDist_image (IsometryEquiv.divLeft x).isometry, ← IsometryEquiv.preimage_symm]
simp
