Commit 2025-05-04 06:34 1aebe697

View on Github →

feat(Topology/Algebra/Valued): Add IsClosed and IsClopen lemmas (#24353) Add lemmas that open balls, closed balls, spheres and the integers of a valued ring are closed and clopen. Rename integer_isOpen and valuationSubring_isOpen to isOpen_integer and isOpen_valuationSubring and deprecate the old names.

Estimated changes

Modified Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean

Modified Mathlib/Topology/Algebra/Valued/ValuationTopology.lean

deleted theorem Valued.integer_isOpen

added theorem Valued.isClopen_ball

added theorem Valued.isClopen_closedBall

added theorem Valued.isClopen_integer

added theorem Valued.isClopen_sphere

added theorem Valued.isClopen_valuationSubring

added theorem Valued.isClosed_ball

added theorem Valued.isClosed_closedBall

added theorem Valued.isClosed_integer

added theorem Valued.isClosed_sphere

added theorem Valued.isClosed_valuationSubring

added theorem Valued.isOpen_integer

modified theorem Valued.isOpen_sphere

added theorem Valued.isOpen_valuationSubring

deleted theorem Valued.valuationSubring_isOpen