[Merged by Bors] - feat(MetricSpace/Ultra): IsUltrametricDist and basic facts on open/closed sets in such spaces

[pechersky]

TODO in future PRs

• add "all triangles are isosceles" in such normed spaces
• totally disconnected space
• give instances of this to Z_p, Q_p, etc

---

[github-actions]

PR summary 00154257b5

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Topology.MetricSpace.Ultra.Basic	858

---

Declarations diff

+ IsUltrametricDist
+ ball_eq_of_mem
+ ball_eq_or_disjoint
+ ball_subset_trichotomy
+ closedBall_eq_of_mem
+ closedBall_eq_or_disjoint
+ closedBall_subset_trichotomy
+ dist_triangle_max
+ frontier_ball_eq_empty
+ frontier_closedBall_eq_empty
+ isClopen_ball
+ isClopen_closedBall
+ isClopen_sphere
+ isClosed_ball
+ isOpen_closedBall
+ isOpen_sphere
+ mem_ball_iff
+ mem_closedBall_iff

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

[j-loreaux]

Thanks! I think there are some easy simplifications that can be made. I'll have another look when you think it's ready again.

[j-loreaux]

Sorry for missing the point of the trichotomy lemmas earlier. Here they are again with short proofs. You are welcome to add them back in.

lemma 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_le 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]

lemma closedBall_subset_trichotomy :
    closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨
    Disjoint (closedBall x r) (closedBall 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_le hrs).le
  · refine Set.disjoint_or_nonempty_inter (closedBall x r) (closedBall y s) |>.symm.imp
      (fun h ↦ ?_) (Or.inr ·)
    obtain ⟨hxz, hyz⟩ := (Set.mem_inter_iff _ _ _).mp h.some_mem
    have hx := closedBall_subset_closedBall hrs (x := x)
    rwa [closedBall_eq_of_mem hyz |>.trans (closedBall_eq_of_mem <| hx hxz).symm]

[j-loreaux]

up to potentially reordering lemmas to make things match better, I'm happy. If you want to reorder go for it, but it's not required.

bors d+

[mathlib-bors]

✌️ pechersky can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[pechersky]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style