mem_sphere_one_iff_norm

Mathlib.Analysis.Normed.Group.Basic

URI: https://scilib.ai/kg/mathlib#mem_sphere_one_iff_norm

English

a ∈ sphere(1, r) iff ‖a‖ = r.

Русский

a принадлежит сфере вокруг единицы радиуса r тогда и только тогда, когда ‖a‖ = r.

LaTeX

$$$$ a \in \mathrm{sphere}(1, r) \iff \|a\| = r. $$$$

Lean4

@[to_additive] -- `simp` can prove this

theorem mem_sphere_one_iff_norm : a ∈ sphere (1 : E) r ↔ ‖a‖ = r := by simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru