English
For balls B(x,r) and B(y,s) in an ultrametric space, exactly one of the following holds: B(x,r) ⊆ B(y,s), or B(y,s) ⊆ B(x,r), or B(x,r) ∩ B(y,s) = ∅.
Русский
Для шаров B(x,r) и B(y,s) в ультраметрическом пространстве выполняется ровно одно из: B(x,r) ⊆ B(y,s), или B(y,s) ⊆ B(x,r), или B(x,r) ∩ B(y,s) = ∅.
LaTeX
$$B(x,r) ⊆ B(y,s) ∨ B(y,s) ⊆ B(x,r) ∨ Disjoint(B(x,r), B(y,s))$$
Lean4
theorem ball_subset_trichotomy : ball x r ⊆ ball y s ∨ ball y s ⊆ ball x r ∨ Disjoint (ball x r) (ball y s) :=
by
wlog hrs : r ≤ s generalizing x y r s
· rw [disjoint_comm, ← or_assoc, or_comm (b := _ ⊆ _), or_assoc]
exact this y x s r (lt_of_not_ge hrs).le
· refine Set.disjoint_or_nonempty_inter (ball x r) (ball y s) |>.symm.imp (fun h ↦ ?_) (Or.inr ·)
obtain ⟨hxz, hyz⟩ := (Set.mem_inter_iff _ _ _).mp h.some_mem
have hx := ball_subset_ball hrs (x := x)
rwa [ball_eq_of_mem hyz |>.trans (ball_eq_of_mem <| hx hxz).symm]
