Mathlib Map

Theorems · Theorem · approximation theory

LinearGrowth.linearGrowthInf_top

LinearGrowth.linearGrowthInf ⊤ = ⊤
Defined in
Mathlib.Analysis.Asymptotics.LinearGrowth
Cited by
5 results in Mathlib
Foundations
Depth 129 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Monotone.linearGrowthInf_nonneg · cited by 4Monotone.linearGrowthInf_…ExpGrowth.expGrowthInf_top · cited by 4ExpGrowth.expGrowthInf_topLinearGrowth.linearGrowthInf_comp_nonneg · cited by 3LinearGrowth.linearGrowth…LinearGrowth.linearGrowthInfTopHom · cited by 1LinearGrowth.linearGrowth…LinearGrowth.linearGrowthInf_biInf · cited by 1LinearGrowth.linearGrowth…LinearGrowth.linearGrowthSup_top · cited by 0LinearGrowth.linearGrowth…Top.top · cited by 9680Top.topEReal · cited by 793ERealNat.cast_pos' · cited by 219Nat.cast_pos'Filter.eventually_atTop · cited by 112Filter.eventually_atTopLinearGrowth.linearGrowthInf · cited by 41LinearGrowth.linearGrowth…EReal.natCast_ne_top · cited by 19EReal.natCast_ne_topFilter.liminf_congr · cited by 14Filter.liminf_congrFilter.liminf_const · cited by 8Filter.liminf_constEReal.top_div_of_pos_ne_top · cited by 1EReal.top_div_of_pos_ne_t…LinearGrowth.linearGrowthInf_…CITED BYCITES

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by6

Results whose statement or proof uses this declaration.