ball_subset_ball' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem ball_subset_ball' (h : ε₁ + dist x y ≤ ε₂) : ball x ε₁ ⊆ ball y ε₂ := fun z hz =>
  calc
    dist z y ≤ dist z x + dist x y := dist_triangle _ _ _
    _ < ε₁ + dist x y := (add_lt_add_right (mem_ball.1 hz) _)
    _ ≤ ε₂ := h

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