Commit 2023-05-26 09:02 e4a716f5

View on Github →

feat: port Topology.MetricSpace.Holder (#4381)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/MetricSpace/Holder.lean

added theorem HolderOnWith.comp

added theorem HolderOnWith.comp_holderWith

added theorem HolderOnWith.ediam_image_inter_le

added theorem HolderOnWith.ediam_image_inter_le_of_le

added theorem HolderOnWith.ediam_image_le

added theorem HolderOnWith.ediam_image_le_of_le

added theorem HolderOnWith.ediam_image_le_of_subset

added theorem HolderOnWith.ediam_image_le_of_subset_of_le

added theorem HolderOnWith.edist_le

added theorem HolderOnWith.edist_le_of_le

added def HolderOnWith

added theorem HolderWith.comp

added theorem HolderWith.comp_holderOnWith

added theorem HolderWith.dist_le

added theorem HolderWith.dist_le_of_le

added theorem HolderWith.ediam_image_le

added theorem HolderWith.edist_le

added theorem HolderWith.edist_le_of_le

added theorem HolderWith.nndist_le

added theorem HolderWith.nndist_le_of_le

added def HolderWith

added theorem Set.Subsingleton.holderOnWith

added theorem holderOnWith_empty

added theorem holderOnWith_one

added theorem holderOnWith_singleton

added theorem holderOnWith_univ

added theorem holderWith_id

added theorem holderWith_one