Commit 2025-07-07 18:08 f2f4294d

View on Github →

feat(Topology/ValuativeRel): helper instance for Valued from ValuativeTopology (#26713) and lemmas on clopen balls

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/Valued/ValuativeRel.lean

added theorem ValuativeTopology.hasBasis_nhds_zero

added theorem ValuativeTopology.isClopen_ball

added theorem ValuativeTopology.isClopen_closedBall

added theorem ValuativeTopology.isClopen_sphere

added theorem ValuativeTopology.isClosed_ball

added theorem ValuativeTopology.isClosed_closedBall

added theorem ValuativeTopology.isOpen_ball

added theorem ValuativeTopology.isOpen_closedBall

added theorem ValuativeTopology.isOpen_sphere

added theorem ValuativeTopology.mem_nhds