Theorem Subtype.preimage_emetricClosedBall

Modification history

2025-11-24 15:10
Mathlib/Topology/EMetricSpace/Defs.lean
feat(MetricSpace): images and preimages of balls in subtypes (#31957)
Added Subtype.preimage_emetricClosedBallView on Github →