Commit 2024-09-19 12:35 0e7d5544

View on Github →

chore: rename Holder to Hoelder (#16870) As indicated by https://en.wikipedia.org/wiki/Germanic_umlaut#Substitution, Hölder should be transcribed to Hoelder in ASCII.

Estimated changes

deleted theorem HolderWith.dimH_image_le
deleted theorem HolderWith.dimH_range_le
added theorem HoelderOnWith.comp
added theorem HoelderOnWith.edist_le
added def HoelderOnWith
added theorem HoelderWith.add
added theorem HoelderWith.comp
added theorem HoelderWith.const
added theorem HoelderWith.dist_le
added theorem HoelderWith.edist_le
added theorem HoelderWith.mono
added theorem HoelderWith.nndist_le
added theorem HoelderWith.of_isEmpty
added theorem HoelderWith.smul
added theorem HoelderWith.zero
added def HoelderWith
deleted theorem HolderOnWith.comp
deleted theorem HolderOnWith.edist_le
deleted def HolderOnWith
deleted theorem HolderWith.add
deleted theorem HolderWith.comp
deleted theorem HolderWith.const
deleted theorem HolderWith.dist_le
deleted theorem HolderWith.dist_le_of_le
deleted theorem HolderWith.ediam_image_le
deleted theorem HolderWith.edist_le
deleted theorem HolderWith.edist_le_of_le
deleted theorem HolderWith.mono
deleted theorem HolderWith.nndist_le
deleted theorem HolderWith.of_isEmpty
deleted theorem HolderWith.smul
deleted theorem HolderWith.zero
deleted def HolderWith
added theorem hoelderOnWith_empty
added theorem hoelderOnWith_one
added theorem hoelderOnWith_univ
added theorem hoelderWith_id
added theorem hoelderWith_one
added theorem hoelderWith_zero_iff
deleted theorem holderOnWith_empty
deleted theorem holderOnWith_one
deleted theorem holderOnWith_singleton
deleted theorem holderOnWith_univ
deleted theorem holderWith_id
deleted theorem holderWith_one
deleted theorem holderWith_zero_iff