Theorems · Theorem · approximation theory
LinearGrowth.linearGrowthSup_bot
LinearGrowth.linearGrowthSup ⊥ = ⊥
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 129 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Bot.botstatement and proof · cited by 4,720
- ERealstatement and proof · cited by 793
- Filter.Eventually.monoproof · cited by 646
- Nat.cast_pos'proof · cited by 219
- Filter.eventually_gt_atTopproof · cited by 90
- LinearGrowth.linearGrowthSupstatement and proof · cited by 38
- Filter.limsup_congrproof · cited by 20
- EReal.natCast_ne_topproof · cited by 19
- Filter.limsup_constproof · cited by 12
- EReal.bot_div_of_pos_ne_topproof · cited by 1
Cited by7
Results whose statement or proof uses this declaration.
- ExpGrowth.expGrowthSup_zeroproof · cited by 6
- LinearGrowth.linearGrowthInf_botproof · cited by 3
- Monotone.le_linearGrowthSup_compproof · cited by 2
- Monotone.linearGrowthSup_compproof · cited by 2
- LinearGrowth.linearGrowthSupBotHomproof · cited by 1
- LinearGrowth.linearGrowthSup_biSupproof · cited by 1
- LinearGrowth.linearGrowthSup_le_of_eventually_leproof · cited by 0