mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(Topology/MetricSpace): Add new file with type of Katetov maps

Open luigi-massacci opened this issue 11 months ago • 0 comments

add a type of Katetov maps (one point extensions of a metric) and related notation and FunLike coercions.

Open in Gitpod

luigi-massacci avatar Mar 06 '24 14:03 luigi-massacci