Theorem ValuativeTopology.isOpen_ball

Modification history

2025-08-04 14:14
Mathlib/Topology/Algebra/Valued/ValuativeRel.lean
chore: rename ValuativeTopology to IsValuativeTopology (#26845)
Deleted ValuativeTopology.isOpen_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.isOpen_ballView on Github →