ball_eq_or_disjoint — Mathlib

English

Two balls of the same radius in an ultrametric space are either equal or disjoint.

Русский

Два шара одинакового радиуса в ультраметрическом пространстве либо равны, либо не пересекаются.

LaTeX

$$ball(x,r) = ball(y,r) ∨ Disjoint(ball(x,r), ball(y,r))$$

Lean4

theorem ball_eq_or_disjoint : ball x r = ball y r ∨ Disjoint (ball x r) (ball y r) :=
  by
  refine Set.disjoint_or_nonempty_inter (ball x r) (ball y r) |>.symm.imp (fun h ↦ ?_) id
  have h₁ := ball_eq_of_mem <| Set.inter_subset_left h.some_mem
  have h₂ := ball_eq_of_mem <| Set.inter_subset_right h.some_mem
  exact h₁.trans h₂.symm

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