Commit 2024-02-08 21:54 bdeb5d97

View on Github →

feat: Characterization of CocompactMap in terms of norms (#10182)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Normed/Group/CocompactMap.lean

added theorem CocompactMapClass.norm_le

added theorem ContinuousMapClass.toCocompactMapClass_of_norm

added theorem Filter.tendsto_cocompact_cocompact_of_norm