ne_one_of_mem_sphere — Mathlib

English

Let E be a seminormed group. If r ≠ 0 and x lies on the sphere with center 1 and radius r, then x ≠ 1.

Русский

Пусть E — полугруппа с нормировкой. Пусть r ≠ 0 и x лежит на сфере с центром в 1 и радиусом r; тогда x ≠ 1.

LaTeX

$$$\\forall E [\\text{SeminormedGroup } E],\\ \\forall r \\in \\mathbb{R},\\ r \\neq 0 \\Rightarrow \\forall x \\in \\mathrm{sphere}(1_E, r),\\: x \\neq 1_E$$$

Lean4

@[to_additive]
theorem ne_one_of_mem_sphere (hr : r ≠ 0) (x : sphere (1 : E) r) : (x : E) ≠ 1 :=
  ne_one_of_norm_ne_zero <| by rwa [norm_eq_of_mem_sphere' x]

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