nonneg_of_mem_sphere

Mathlib.Topology.MetricSpace.Pseudo.Defs

URI: https://scilib.ai/kg/mathlib#Metric.nonneg_of_mem_sphere

English

If a point y lies on the sphere with center x and radius ε, then ε is nonnegative.

Русский

Если точка y лежит на сфере с центром в x и радиусом ε, то ε неотрицательно.

LaTeX

$$$(y \\in \\mathrm{sphere}(x, \\varepsilon)) \\Rightarrow 0 \\le \\varepsilon$$$

Lean4

theorem nonneg_of_mem_sphere (hy : y ∈ sphere x ε) : 0 ≤ ε :=
  dist_nonneg.trans_eq hy

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

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

Разделы

Аффилиация

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