Commit 2024-09-05 13:22 3f81e054

View on Github →

chore: split out Topology.EMetricSpace.Pi (#16507)

Estimated changes

deleted theorem edist_le_pi_edist
deleted theorem edist_pi_const
deleted theorem edist_pi_const_le
deleted theorem edist_pi_def
deleted theorem edist_pi_le_iff
added theorem edist_le_pi_edist
added theorem edist_pi_const
added theorem edist_pi_const_le
added theorem edist_pi_def
added theorem edist_pi_le_iff