closedBall_eq_or_disjoint — Mathlib

English

Two closed balls of the same radius are either equal or disjoint.

Русский

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

LaTeX

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

Lean4

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

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