dist_lt_add_of_nonempty_closedBall_inter_ball

English

If the intersection of the closed ball B̄(x, ε1) and the closed ball 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)).Nonempty → dist(x, y) ≤ \varepsilon_1 + \varepsilon_2 $$$

Lean4

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

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