Commit 2024-10-04 11:14 10237afb

View on Github →

feat (Analysis/Normed/Group): ultrametric normed groups are nonarchimedean (#17262) This PR proves that normed groups with a norm satisfying IsUltrametricDist are nonarchimedean topological groups, and also that continuous maps from a compact space to an ultrametric space are an ultrametric space.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Normed/Group/Ultra.lean

added def IsUltrametricDist.ball_openSubgroup

added def IsUltrametricDist.closedBall_openSubgroup

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