norm_eq_of_zero — Mathlib

English

When p = 0, the norm on AddCircle (0) coincides with the absolute value on ℝ: ‖(x : AddCircle (0))‖ = |x|.

Русский

При p = 0 норма на AddCircle(0) совпадает с абсолютной величиной на ℝ: ‖(x : AddCircle(0))‖ = |x|.

LaTeX

$$$$\\| (x : \\mathrm{AddCircle}(0)) \\| = |x|.$$$$

Lean4

@[simp]
theorem norm_eq_of_zero {x : ℝ} : ‖(x : AddCircle (0 : ℝ))‖ = |x| :=
  by
  suffices {y : ℝ | (y : AddCircle (0 : ℝ)) = (x : AddCircle (0 : ℝ))} = { x } by simp [norm_eq_infDist, this]
  ext y
  simp [eq_iff_sub_mem, sub_eq_zero]

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