Mathlib Changelog
v4
Changelog
About
Github
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