pos_of_mem_ball

Mathlib.Topology.EMetricSpace.Defs

URI: https://scilib.ai/kg/mathlib#EMetric.pos_of_mem_ball

English

If y lies in ball(x,ε), then ε > 0.

Русский

Если y принадлежит ball(x,ε), то ε > 0.

LaTeX

$$$ y \in \operatorname{ball}(x,\varepsilon) \Rightarrow 0 < \varepsilon. $$$

Lean4

theorem pos_of_mem_ball (hy : y ∈ ball x ε) : 0 < ε :=
  lt_of_le_of_lt (zero_le _) hy

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

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

Разделы

Аффилиация

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