closedBall_subset_ball' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem closedBall_subset_ball' (h : ε₁ + dist x y < ε₂) : closedBall x ε₁ ⊆ ball 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

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