Commit 2025-11-24 15:10 d9c357f4

View on Github →

feat(MetricSpace): images and preimages of balls in subtypes (#31957)

Estimated changes

Modified Mathlib/Topology/EMetricSpace/Defs.lean

added theorem Subtype.image_emetricBall

added theorem Subtype.image_emetricClosedBall

added theorem Subtype.preimage_emetricBall

added theorem Subtype.preimage_emetricClosedBall

Modified Mathlib/Topology/MetricSpace/Pseudo/Constructions.lean

modified theorem Subtype.dist_eq

added theorem Subtype.image_ball

added theorem Subtype.image_closedBall

modified theorem Subtype.nndist_eq

added theorem Subtype.preimage_ball

added theorem Subtype.preimage_closedBall