Commit 2024-07-18 14:24 3e979fb1

View on Github →

feat(MetricSpace/Ultra): IsUltrametricDist and basic facts on open/closed sets in such spaces (#14433) 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

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/MetricSpace/Ultra/Basic.lean

added theorem IsUltrametricDist.ball_eq_of_mem

added theorem IsUltrametricDist.ball_eq_or_disjoint

added theorem IsUltrametricDist.ball_subset_trichotomy

added theorem IsUltrametricDist.closedBall_eq_of_mem

added theorem IsUltrametricDist.closedBall_eq_or_disjoint

added theorem IsUltrametricDist.closedBall_subset_trichotomy

added theorem IsUltrametricDist.frontier_ball_eq_empty

added theorem IsUltrametricDist.frontier_closedBall_eq_empty

added theorem IsUltrametricDist.isClopen_ball

added theorem IsUltrametricDist.isClopen_closedBall

added theorem IsUltrametricDist.isClopen_sphere

added theorem IsUltrametricDist.isClosed_ball

added theorem IsUltrametricDist.isOpen_closedBall

added theorem IsUltrametricDist.isOpen_sphere

added theorem IsUltrametricDist.mem_ball_iff

added theorem IsUltrametricDist.mem_closedBall_iff

added theorem dist_triangle_max