Theorem Homeomorph.isClosed_setOf_iff

Modification history

2025-11-27 16:30

Mathlib/Topology/Homeomorph/Defs.lean

feat: `PadicInt` is isomorphic to the integers of the uniform space completion `(Rat.padicValuation p).Completion` (#30363) …

Added Homeomorph.isClosed_setOf_iff View on Github →