ball_half_subset

Mathlib.Topology.MetricSpace.Pseudo.Defs

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

English

If y lies in the ball around x with radius ε/2, then the ball around y with radius ε/2 is contained in the ball around x with radius ε.

Русский

Если y ∈ B(x, ε/2), то B(y, ε/2) ⊆ B(x, ε).

LaTeX

$$$ y \in B(x, \frac{ε}{2}) \Rightarrow B(y, \frac{ε}{2}) \subseteq B(x, ε) $$$

Lean4

theorem ball_half_subset (y) (h : y ∈ ball x (ε / 2)) : ball y (ε / 2) ⊆ ball x ε :=
  ball_subset <| by rw [sub_self_div_two]; exact le_of_lt h

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

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

Разделы

Аффилиация

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