Commit 2023-06-24 07:45 5f4d5df8

View on Github →

feat: port Topology.MetricSpace.Dilation (#5442)

Estimated changes

added theorem Dilation.antilipschitz
added theorem Dilation.cancel_left
added theorem Dilation.cancel_right
added theorem Dilation.coe_comp
added theorem Dilation.coe_id
added theorem Dilation.coe_mk
added theorem Dilation.coe_mul
added theorem Dilation.coe_one
added def Dilation.comp
added theorem Dilation.comp_apply
added theorem Dilation.comp_assoc
added theorem Dilation.comp_id
added theorem Dilation.comp_ratio
added theorem Dilation.congr_arg
added theorem Dilation.congr_fun
added theorem Dilation.copy_eq_self
added theorem Dilation.diam_image
added theorem Dilation.diam_range
added theorem Dilation.dist_eq
added theorem Dilation.ediam_image
added theorem Dilation.ediam_range
added theorem Dilation.edist_eq
added theorem Dilation.ext
added theorem Dilation.ext_iff
added theorem Dilation.id_comp
added theorem Dilation.id_ratio
added theorem Dilation.lipschitz
added theorem Dilation.mapsTo_ball
added theorem Dilation.mapsTo_sphere
added theorem Dilation.mk_coe
added theorem Dilation.mul_def
added theorem Dilation.nndist_eq
added theorem Dilation.one_def
added def Dilation.ratio
added theorem Dilation.ratio_ne_zero
added theorem Dilation.ratio_pos
added theorem Dilation.ratio_unique
added theorem Dilation.toContinuous
added theorem Dilation.toFun_eq_coe
added structure Dilation