closedBall_subset_ball

Mathlib.Topology.MetricSpace.Pseudo.Defs

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

English

If ε1 < ε2, then the closed ball around x of radius ε1 is contained in the ball around x of radius ε2.

Русский

Если ε1 < ε2, то B̄(x, ε1) ⊆ B(x, ε2).

LaTeX

$$$ \overline{B}(x, \varepsilon_1) \subseteq B(x, \varepsilon_2) \quad\text{if } \varepsilon_1 < \varepsilon_2 $$$

Lean4

theorem closedBall_subset_ball (h : ε₁ < ε₂) : closedBall x ε₁ ⊆ ball x ε₂ := fun y (yh : dist y x ≤ ε₁) =>
  lt_of_le_of_lt yh h

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

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

Разделы

Аффилиация

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