dist_le_add_of_nonempty_closedBall_inter_closedBall

English

If the intersection of the closed balls B̄(x, ε1) and B̄(y, ε2) is nonempty, then dist(x, y) ≤ ε1 + ε2.

Русский

Если пересечение замкнутых шаров B̄(x, ε1) ∩ B̄(y, ε2) непусто, то dist(x, y) ≤ ε1 + ε2.

LaTeX

$$$ (\overline{B}(x, \varepsilon_1) \cap \overline{B}(y, \varepsilon_2)) \neq \emptyset \Rightarrow \operatorname{dist}(x, y) \le \varepsilon_1 + \varepsilon_2 $$$

Lean4

theorem dist_le_add_of_nonempty_closedBall_inter_closedBall (h : (closedBall x ε₁ ∩ closedBall y ε₂).Nonempty) :
    dist x y ≤ ε₁ + ε₂ :=
  let ⟨z, hz⟩ := h
  calc
    dist x y ≤ dist z x + dist z y := dist_triangle_left _ _ _
    _ ≤ ε₁ + ε₂ := add_le_add hz.1 hz.2

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