ZeroAtInfty

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

Statistics

Metric	Count
Definitions	0
Theorems norm_le, zero_at_infty_of_norm_le	2
Total	2

ZeroAtInftyContinuousMapClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm_le 📖	mathematical	Real Real.instLT Real.instZero	Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe	—	zero_at_infty Metric.closedBall_compl_subset_of_mem_cocompact Filter.tendsto_def tendsto_zero_iff_norm_tendsto_zero Metric.ball_mem_nhds dist_zero_right norm_norm

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
zero_at_infty_of_norm_le 📖	mathematical	Real Real.instLT Norm.norm SeminormedAddCommGroup.toNorm	Filter.Tendsto Filter.cocompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace nhds SeminormedAddCommGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	tendsto_zero_iff_norm_tendsto_zero Filter.mem_map Metric.mem_cocompact_iff_closedBall_compl_subset Metric.mem_nhds_iff dist_zero_right norm_norm

---

← Back to Index