Theorem ValuativeTopology.isClosed_ball

Modification history

2025-08-04 14:14
Mathlib/Topology/Algebra/Valued/ValuativeRel.lean
chore: rename ValuativeTopology to IsValuativeTopology (#26845)
Deleted ValuativeTopology.isClosed_ballView on Github →
2025-07-07 18:08
Mathlib/Topology/Algebra/Valued/ValuativeRel.lean
feat(Topology/ValuativeRel): helper instance for Valued from ValuativeTopology (#26713) …
Added ValuativeTopology.isClosed_ballView on Github →