mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(MetricSpace/Ultra): IsUltrametricDist and basic facts on open/closed sets in such spaces

Open pechersky opened this issue 1 year ago • 1 comments

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

Open in Gitpod

pechersky avatar Jul 05 '24 00:07 pechersky