norm_eq_of_mem_sphere' — Mathlib

English

Let E be a seminormed group and r ∈ R. If x lies on the sphere centered at 1 with radius r, then the norm of x equals r.

Русский

Пусть E — полугруппа с нормировкой и r ∈ ℝ. Если x лежит на сфере с центром в 1 и радиусом r, то ‖x‖ = r.

LaTeX

$$$\\forall x \\in \\mathrm{sphere}(1_E, r),\\: \\|x\\| = r$$$

Lean4

@[to_additive (attr := simp) norm_eq_of_mem_sphere]
theorem norm_eq_of_mem_sphere' (x : sphere (1 : E) r) : ‖(x : E)‖ = r :=
  mem_sphere_one_iff_norm.mp x.2

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