dist_lt_add_of_nonempty_ball_inter_ball

English

If the intersection of the open 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

$$$ (B(x, \varepsilon_1) \cap B(y, \varepsilon_2)).Nonempty → dist(x, y) < \varepsilon_1 + \varepsilon_2 $$$

Lean4

theorem dist_lt_add_of_nonempty_ball_inter_ball (h : (ball x ε₁ ∩ ball y ε₂).Nonempty) : dist x y < ε₁ + ε₂ :=
  dist_lt_add_of_nonempty_closedBall_inter_ball <| h.mono (inter_subset_inter ball_subset_closedBall Subset.rfl)

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