mem_sphere_iff_norm'

Mathlib.Analysis.Normed.Group.Basic

URI: https://scilib.ai/kg/mathlib#mem_sphere_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 (attr := simp high) mem_sphere_iff_norm]
theorem mem_sphere_iff_norm' : b ∈ sphere a r ↔ ‖b / a‖ = r := by simp [dist_eq_norm_div]

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

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

Разделы

Аффилиация

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