ball_eq_of_mem — Mathlib

English

If y lies in the open ball B(x,r) in an ultrametric space, then B(x,r) = B(y,r).

Русский

Пусть y принадлежит открытому шару B(x,r) в ультраметрическом пространстве; тогда B(x,r) = B(y,r).

LaTeX

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

Lean4

theorem ball_eq_of_mem {x y : X} {r : ℝ} (h : y ∈ ball x r) : ball x r = ball y r :=
  by
  ext a
  simp_rw [mem_ball] at h ⊢
  constructor <;> intro h' <;> exact (dist_triangle_max _ _ _).trans_lt (max_lt h' (dist_comm x _ ▸ h))

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