Commit 2024-09-20 00:43 0f3d1c6a

View on Github →

chore: revert holder -> hoelder (#16955) Per https://leanprover.zulipchat.com/#narrow/stream/116290-rss/topic/Recent.20Commits.20to.20mathlib4.3Amaster/near/471490433

Estimated changes

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