CocompactMap

📁 Source: Mathlib/Analysis/Normed/Group/CocompactMap.lean

Statistics

Metric	Count
Definitions	0
Theorems norm_le, toCocompactMapClass_of_norm, tendsto_cocompact_cocompact_of_norm	3
Total	3

CocompactMapClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm_le 📖	mathematical	—	Real Real.instLT Norm.norm NormedAddCommGroup.toNorm DFunLike.coe	—	cocompact_tendsto Metric.closedBall_compl_subset_of_mem_cocompact Filter.tendsto_def Metric.mem_cocompact_of_closedBall_compl_subset Eq.subset Set.instReflSubset dist_zero_right

ContinuousMapClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toCocompactMapClass_of_norm 📖	mathematical	Real Real.instLT Norm.norm NormedAddCommGroup.toNorm DFunLike.coe	CocompactMapClass UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	Filter.tendsto_cocompact_cocompact_of_norm

Filter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tendsto_cocompact_cocompact_of_norm 📖	mathematical	Real Real.instLT Norm.norm NormedAddCommGroup.toNorm	Tendsto cocompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	tendsto_def Metric.closedBall_compl_subset_of_mem_cocompact Metric.mem_cocompact_of_closedBall_compl_subset dist_zero_right

---

← Back to Index