Commit 2023-03-07 16:09 187c3ef6

View on Github →

feat: port Topology.MetricSpace.Antilipschitz (#2635)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/MetricSpace/Antilipschitz.lean

added theorem AntilipschitzWith.bounded_preimage

added theorem AntilipschitzWith.closedEmbedding

added theorem AntilipschitzWith.codRestrict

added theorem AntilipschitzWith.comap_uniformity_le

added theorem AntilipschitzWith.comp

added theorem AntilipschitzWith.ediam_preimage_le

added theorem AntilipschitzWith.edist_lt_top

added theorem AntilipschitzWith.edist_ne_top

added theorem AntilipschitzWith.isClosed_range

added theorem AntilipschitzWith.isComplete_range

added theorem AntilipschitzWith.le_mul_ediam_image

added theorem AntilipschitzWith.mul_le_dist

added theorem AntilipschitzWith.mul_le_edist

added theorem AntilipschitzWith.mul_le_nndist

added theorem AntilipschitzWith.of_subsingleton

added theorem AntilipschitzWith.restrict

added theorem AntilipschitzWith.subtype_coe

added theorem AntilipschitzWith.tendsto_cobounded

added theorem AntilipschitzWith.to_rightInvOn

added theorem AntilipschitzWith.to_rightInverse

added theorem AntilipschitzWith.to_right_inv_on'

added def AntilipschitzWith

added theorem LipschitzWith.to_rightInverse

added theorem antilipschitzWith_iff_le_mul_dist

added theorem antilipschitzWith_iff_le_mul_nndist