Theorem ValuativeTopology.isOpen_sphere

Modification history

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