closedBall_subset_closedBall' — Mathlib

English

If ε1 + dist(x,y) ≤ ε2, then the closed ball around x of radius ε1 is contained in the closed ball around y of radius ε2.

Русский

Если ε1 + dist(x,y) ≤ ε2, то B̄(x, ε1) ⊆ B̄(y, ε2).

LaTeX

$$$ \overline{B}(x, \varepsilon_1) \subseteq \overline{B}(y, \varepsilon_2) \quad\text{if } \varepsilon_1 + dist(x,y) \le \varepsilon_2 $$$

Lean4

theorem closedBall_subset_closedBall' (h : ε₁ + dist x y ≤ ε₂) : closedBall x ε₁ ⊆ closedBall y ε₂ := fun z hz =>
  calc
    dist z y ≤ dist z x + dist x y := dist_triangle _ _ _
    _ ≤ ε₁ + dist x y := (add_le_add_right (mem_closedBall.1 hz) _)
    _ ≤ ε₂ := h

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