norm_eq — Mathlib

English

For any real x, the norm in UnitAddCircle equals the distance to the nearest integer, i.e., ‖x‖ = |x − round(x)|.

Русский

Для любого действительного x норма в UnitAddCircle равна расстоянию до ближайшего целого: ‖x‖ = |x − round(x)|.

LaTeX

$$$\\| x : \\mathrm{UnitAddCircle} \\| = |x - \\operatorname{round}(x)|$$$

Lean4

theorem norm_eq {x : ℝ} : ‖(x : UnitAddCircle)‖ = |x - round x| := by simp [AddCircle.norm_eq]

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