closedBall_eq_of_mem — Mathlib

English

If y belongs to the closed ball, then the closed balls around x and y with the same radius are equal.

Русский

Если y принадлежит замкнутому шару, то замкнутые шары вокруг x и y с одинаковым радиусом равны.

LaTeX

$$y \in \overline{\mathrm{ball}}(x,r) \Rightarrow \overline{\mathrm{ball}}(x,r) = \overline{\mathrm{ball}}(y,r)$$

Lean4

theorem closedBall_eq_of_mem {x y : X} {r : ℝ} (h : y ∈ closedBall x r) : closedBall x r = closedBall y r :=
  by
  ext
  simp_rw [mem_closedBall] at h ⊢
  constructor <;> intro h' <;> exact (dist_triangle_max _ _ _).trans (max_le h' (dist_comm x _ ▸ h))

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