LinearGrowth

📁 Source: Mathlib/Analysis/Asymptotics/LinearGrowth.lean

Statistics

Metric	Count
Definitions `linearGrowthInf`, `linearGrowthInfTopHom`, `linearGrowthSup`, `linearGrowthSupBotHom`	4
Theorems `le_linearGrowthInf`, `linearGrowthSup_le`, `le_linearGrowthSup`, `linearGrowthInf_le`, `eventually_atTop_exists_nat_between`, `eventually_atTop_exists_int_between`, `eventually_atTop_exists_nat_between`, `eventually_le_mul`, `eventually_mul_le`, `frequently_le_mul`, `frequently_mul_le`, `le_linearGrowthInf_add`, `le_linearGrowthInf_comp`, `le_linearGrowthInf_iff`, `le_linearGrowthSup_add`, `le_linearGrowthSup_add'`, `le_linearGrowthSup_iff`, `linearGrowthInf_add_le`, `linearGrowthInf_add_le'`, `linearGrowthInf_biInf`, `linearGrowthInf_bot`, `linearGrowthInf_comp_nonneg`, `linearGrowthInf_congr`, `linearGrowthInf_const`, `linearGrowthInf_const_mul_self`, `linearGrowthInf_eventually_monotone`, `linearGrowthInf_iInf`, `linearGrowthInf_inf`, `linearGrowthInf_le_iff`, `linearGrowthInf_le_linearGrowthSup`, `linearGrowthInf_le_linearGrowthSup_of_frequently_le`, `linearGrowthInf_le_of_eventually_le`, `linearGrowthInf_monotone`, `linearGrowthInf_natCast_nonneg`, `linearGrowthInf_neg`, `linearGrowthInf_top`, `linearGrowthInf_zero`, `linearGrowthSup_add_le`, `linearGrowthSup_biSup`, `linearGrowthSup_bot`, `linearGrowthSup_comp_le`, `linearGrowthSup_comp_nonneg`, `linearGrowthSup_congr`, `linearGrowthSup_const`, `linearGrowthSup_const_mul_self`, `linearGrowthSup_eventually_monotone`, `linearGrowthSup_iSup`, `linearGrowthSup_inv`, `linearGrowthSup_le_iff`, `linearGrowthSup_le_of_eventually_le`, `linearGrowthSup_monotone`, `linearGrowthSup_sup`, `linearGrowthSup_top`, `linearGrowthSup_zero`, `tendsto_atTop_of_linearGrowthInf_natCast_pos`, `tendsto_atTop_of_linearGrowthInf_pos`, `le_linearGrowthSup_comp`, `linearGrowthInf_comp`, `linearGrowthInf_comp_le`, `linearGrowthInf_comp_mul`, `linearGrowthInf_nonneg`, `linearGrowthSup_comp`, `linearGrowthSup_comp_mul`, `linearGrowthSup_nonneg`	64
Total	68

Eventually

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_linearGrowthInf` 📖	mathematical	`Filter.Eventually` `EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `EReal.instMul` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `Filter.atTop` `Nat.instPreorder`	`LinearGrowth.linearGrowthInf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid`	—	`LinearGrowth.le_linearGrowthInf_iff` `Filter.Eventually.mono` `LE.le.trans'` `mul_le_mul_of_nonneg_right` `EReal.instMulPosMono` `le_of_lt` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoidEReal` `instZeroLEOneClassEReal`
`linearGrowthSup_le` 📖	mathematical	`Filter.Eventually` `EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `EReal.instMul` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `Filter.atTop` `Nat.instPreorder`	`LinearGrowth.linearGrowthSup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid`	—	`LinearGrowth.linearGrowthSup_le_iff` `Filter.Eventually.mono` `LE.le.trans` `mul_le_mul_of_nonneg_right` `EReal.instMulPosMono` `le_of_lt` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoidEReal` `instZeroLEOneClassEReal`

Frequently

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_linearGrowthSup` 📖	mathematical	`Filter.Frequently` `EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `EReal.instMul` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `Filter.atTop` `Nat.instPreorder`	`LinearGrowth.linearGrowthSup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid`	—	`LinearGrowth.le_linearGrowthSup_iff` `Filter.Frequently.mono` `LE.le.trans'` `mul_le_mul_of_nonneg_right` `EReal.instMulPosMono` `le_of_lt` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoidEReal` `instZeroLEOneClassEReal`
`linearGrowthInf_le` 📖	mathematical	`Filter.Frequently` `EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `EReal.instMul` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `Filter.atTop` `Nat.instPreorder`	`LinearGrowth.linearGrowthInf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid`	—	`LinearGrowth.linearGrowthInf_le_iff` `Filter.Frequently.mono` `LE.le.trans` `mul_le_mul_of_nonneg_right` `EReal.instMulPosMono` `le_of_lt` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoidEReal` `instZeroLEOneClassEReal`

LinearGrowth

Definitions

Name	Category	Theorems
`linearGrowthInf` 📖	CompOp	36 math math: `linearGrowthInf_add_le'`, `le_linearGrowthSup_add`, `le_linearGrowthSup_add'`, `linearGrowthInf_bot`, `linearGrowthInf_biInf`, `linearGrowthInf_le_linearGrowthSup`, `Eventually.le_linearGrowthInf`, `linearGrowthInf_top`, `linearGrowthInf_const_mul_self`, `linearGrowthInf_zero`, `linearGrowthSup_inv`, `linearGrowthInf_const`, `ExpGrowth.le_expGrowthInf_comp`, `linearGrowthInf_inf`, `linearGrowthInf_natCast_nonneg`, `Monotone.linearGrowthInf_nonneg`, `linearGrowthInf_eventually_monotone`, `linearGrowthInf_iInf`, `linearGrowthInf_monotone`, `linearGrowthInf_congr`, `linearGrowthInf_comp_nonneg`, `le_linearGrowthInf_iff`, `ExpGrowth.expGrowthInf_def`, `linearGrowthInf_le_of_eventually_le`, `linearGrowthInf_le_iff`, `Monotone.linearGrowthInf_comp_le`, `Monotone.linearGrowthInf_comp_mul`, `linearGrowthInf_add_le`, `Frequently.linearGrowthInf_le`, `Monotone.linearGrowthInf_comp`, `Monotone.le_linearGrowthSup_comp`, `linearGrowthInf_le_linearGrowthSup_of_frequently_le`, `le_linearGrowthInf_comp`, `le_linearGrowthInf_add`, `linearGrowthInf_neg`, `Monotone.le_expGrowthSup_comp`
`linearGrowthInfTopHom` 📖	CompOp	—
`linearGrowthSup` 📖	CompOp	35 math math: `linearGrowthSup_zero`, `linearGrowthSup_top`, `linearGrowthInf_add_le'`, `le_linearGrowthSup_add`, `linearGrowthSup_add_le`, `le_linearGrowthSup_add'`, `linearGrowthSup_bot`, `linearGrowthInf_le_linearGrowthSup`, `ExpGrowth.expGrowthSup_def`, `Eventually.linearGrowthSup_le`, `linearGrowthSup_le_of_eventually_le`, `linearGrowthSup_biSup`, `linearGrowthSup_inv`, `linearGrowthSup_le_iff`, `linearGrowthSup_const_mul_self`, `linearGrowthSup_congr`, `linearGrowthSup_sup`, `linearGrowthSup_eventually_monotone`, `linearGrowthSup_const`, `linearGrowthSup_comp_nonneg`, `ExpGrowth.expGrowthSup_comp_le`, `Monotone.expGrowthInf_comp_le`, `linearGrowthSup_iSup`, `linearGrowthSup_comp_le`, `Monotone.linearGrowthInf_comp_le`, `linearGrowthInf_add_le`, `Monotone.linearGrowthSup_nonneg`, `Monotone.linearGrowthSup_comp_mul`, `Monotone.le_linearGrowthSup_comp`, `Monotone.linearGrowthSup_comp`, `linearGrowthSup_monotone`, `linearGrowthInf_le_linearGrowthSup_of_frequently_le`, `le_linearGrowthSup_iff`, `Frequently.le_linearGrowthSup`, `linearGrowthInf_neg`
`linearGrowthSupBotHom` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eventually_le_mul` 📖	mathematical	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `linearGrowthSup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal`	`Filter.Eventually` `Preorder.toLE` `EReal.instMul` `Filter.atTop` `Nat.instPreorder`	—	`linearGrowthSup_le_iff` `le_refl`
`eventually_mul_le` 📖	mathematical	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `linearGrowthInf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal`	`Filter.Eventually` `Preorder.toLE` `EReal.instMul` `Filter.atTop` `Nat.instPreorder`	—	`le_linearGrowthInf_iff` `le_refl`
`frequently_le_mul` 📖	mathematical	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `linearGrowthInf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal`	`Filter.Frequently` `Preorder.toLE` `EReal.instMul` `Filter.atTop` `Nat.instPreorder`	—	`linearGrowthInf_le_iff` `le_refl`
`frequently_mul_le` 📖	mathematical	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `linearGrowthSup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal`	`Filter.Frequently` `Preorder.toLE` `EReal.instMul` `Filter.atTop` `Nat.instPreorder`	—	`le_linearGrowthSup_iff` `le_refl`
`le_linearGrowthInf_add` 📖	mathematical	—	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidEReal` `linearGrowthInf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `Pi.instAdd`	—	`LE.le.trans_eq` `EReal.le_liminf_add` `Filter.liminf_congr` `Filter.Eventually.of_forall` `Pi.add_apply` `EReal.add_div_of_nonneg_right` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoidEReal` `instZeroLEOneClassEReal`
`le_linearGrowthInf_comp` 📖	mathematical	`Filter.EventuallyLE` `EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `Filter.atTop` `Nat.instPreorder` `Pi.instZero` `instZeroEReal` `Filter.Tendsto`	`EReal.instMul` `linearGrowthInf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal`	—	`linearGrowthInf_const` `EReal.zero_ne_bot` `EReal.zero_ne_top` `linearGrowthInf_eventually_monotone` `Filter.Tendsto.eventually` `EReal.mul_le_of_forall_lt_of_nonneg` `linearGrowthInf_natCast_nonneg` `Eventually.le_linearGrowthInf` `Filter.eventually_map` `Filter.Eventually.filter_mono` `eventually_mul_le` `Filter.mp_mem` `Filter.eventually_gt_atTop` `instNoTopOrderOfNoMaxOrder` `Nat.instNoMaxOrder` `Filter.eventually_lt_of_lt_liminf` `Filter.isBounded_ge_of_bot` `Filter.univ_mem'` `LT.lt.le` `EReal.lt_div_iff` `Nat.cast_pos'` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoidEReal` `instZeroLEOneClassEReal` `NeZero.charZero_one` `instCharZeroEReal` `EReal.natCast_ne_top` `mul_comm` `mul_assoc` `LE.le.trans'` `mul_le_mul_of_nonneg_left` `EReal.instPosMulMono` `le_of_lt`
`le_linearGrowthInf_iff` 📖	mathematical	—	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `linearGrowthInf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `Filter.Eventually` `EReal.instMul` `Filter.atTop` `Nat.instPreorder`	—	`linearGrowthInf.eq_1` `Filter.le_liminf_iff'` `instDenselyOrderedEReal` `Filter.isCobounded_ge_of_top` `Filter.isBounded_ge_of_bot` `Filter.eventually_congr` `Filter.eventually_atTop` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `EReal.le_div_iff_mul_le` `Nat.cast_zero` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoidEReal` `instZeroLEOneClassEReal` `instCharZeroEReal` `EReal.natCast_ne_top`
`le_linearGrowthSup_add` 📖	mathematical	—	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidEReal` `linearGrowthSup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `linearGrowthInf` `Pi.instAdd`	—	`LE.le.trans_eq` `EReal.le_limsup_add` `Filter.limsup_congr` `Filter.Eventually.of_forall` `Pi.add_apply` `EReal.add_div_of_nonneg_right` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoidEReal` `instZeroLEOneClassEReal`
`le_linearGrowthSup_add'` 📖	mathematical	—	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidEReal` `linearGrowthInf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `linearGrowthSup` `Pi.instAdd`	—	`add_comm` `le_linearGrowthSup_add`
`le_linearGrowthSup_iff` 📖	mathematical	—	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `linearGrowthSup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `Filter.Frequently` `EReal.instMul` `Filter.atTop` `Nat.instPreorder`	—	`linearGrowthSup.eq_1` `Filter.le_limsup_iff'` `instDenselyOrderedEReal` `Filter.isCobounded_le_of_bot` `Filter.isBounded_le_of_top` `Filter.frequently_congr` `Filter.eventually_atTop` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `EReal.le_div_iff_mul_le` `Nat.cast_zero` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoidEReal` `instZeroLEOneClassEReal` `instCharZeroEReal` `EReal.natCast_ne_top`
`linearGrowthInf_add_le` 📖	mathematical	—	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `linearGrowthInf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidEReal` `linearGrowthSup`	—	`LE.le.trans_eq'` `EReal.liminf_add_le` `Filter.liminf_congr` `Filter.Eventually.of_forall` `Pi.add_apply` `EReal.add_div_of_nonneg_right` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoidEReal` `instZeroLEOneClassEReal`
`linearGrowthInf_add_le'` 📖	mathematical	—	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `linearGrowthInf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidEReal` `linearGrowthSup`	—	`add_comm` `linearGrowthInf_add_le`
`linearGrowthInf_biInf` 📖	mathematical	—	`linearGrowthInf` `EReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `iInf` `Pi.infSet` `instInfSetEReal` `Set` `Set.instMembership`	—	`map_finset_inf` `InfTopHom.instInfTopHomClass` `linearGrowthInf_inf` `linearGrowthInf_top` `Finset.inf_eq_iInf` `iInf_congr_Prop` `Set.Finite.mem_toFinset`
`linearGrowthInf_bot` 📖	mathematical	—	`linearGrowthInf` `EReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `Bot.bot` `Pi.instBotForall` `instBotEReal`	—	`le_bot_iff` `linearGrowthSup_bot` `linearGrowthInf_le_linearGrowthSup` `Filter.isBounded_le_of_top` `Filter.isBounded_ge_of_bot`
`linearGrowthInf_comp_nonneg` 📖	mathematical	`Monotone` `EReal` `Nat.instPreorder` `PartialOrder.toPreorder` `instPartialOrderEReal` `Filter.Tendsto` `Filter.atTop`	`Preorder.toLE` `instZeroEReal` `linearGrowthInf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal`	—	`Filter.Eventually.filter_mono` `Filter.eventually_atTop` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `LE.le.trans'` `linearGrowthInf_eventually_monotone` `eq_or_ne` `Pi.top_def` `linearGrowthInf_top` `le_top` `linearGrowthInf_const` `le_refl`
`linearGrowthInf_congr` 📖	mathematical	`Filter.EventuallyEq` `Filter.atTop` `Nat.instPreorder`	`linearGrowthInf`	—	`Filter.liminf_congr` `Filter.Eventually.mono`
`linearGrowthInf_const` 📖	mathematical	—	`linearGrowthInf` `EReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `instZeroEReal`	—	`Filter.Tendsto.liminf_eq` `EReal.instOrderTopology` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `EReal.tendsto_const_div_atTop_nhds_zero_nat`
`linearGrowthInf_const_mul_self` 📖	mathematical	—	`linearGrowthInf` `EReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `EReal.instMul`	—	`le_antisymm` `Frequently.linearGrowthInf_le` `Filter.Frequently.of_forall` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `le_refl` `Eventually.le_linearGrowthInf` `Filter.Eventually.of_forall`
`linearGrowthInf_eventually_monotone` 📖	mathematical	`Filter.EventuallyLE` `EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `Filter.atTop` `Nat.instPreorder`	`linearGrowthInf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal`	—	`Filter.liminf_le_liminf` `Filter.Eventually.mono` `EReal.monotone_div_right_of_nonneg` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoidEReal` `instZeroLEOneClassEReal` `Filter.isBounded_ge_of_bot` `Filter.isCobounded_ge_of_top`
`linearGrowthInf_iInf` 📖	mathematical	—	`linearGrowthInf` `EReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `iInf` `Pi.infSet` `instInfSetEReal`	—	`iInf_univ` `linearGrowthInf_biInf` `Set.finite_univ`
`linearGrowthInf_inf` 📖	mathematical	—	`linearGrowthInf` `EReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `Pi.instMinForall_mathlib` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice`	—	`linearGrowthInf.eq_1` `liminf_min` `Filter.isCobounded_ge_of_top` `Filter.isBounded_ge_of_bot` `Filter.liminf_congr` `Filter.Eventually.of_forall` `Monotone.map_min` `EReal.monotone_div_right_of_nonneg` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoidEReal` `instZeroLEOneClassEReal`
`linearGrowthInf_le_iff` 📖	mathematical	—	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `linearGrowthInf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `Filter.Frequently` `EReal.instMul` `Filter.atTop` `Nat.instPreorder`	—	`linearGrowthInf.eq_1` `Filter.liminf_le_iff'` `instDenselyOrderedEReal` `Filter.isCobounded_ge_of_top` `Filter.isBounded_ge_of_bot` `Filter.frequently_congr` `Filter.eventually_atTop` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `EReal.div_le_iff_le_mul` `Nat.cast_zero` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoidEReal` `instZeroLEOneClassEReal` `instCharZeroEReal` `EReal.natCast_ne_top` `mul_comm`
`linearGrowthInf_le_linearGrowthSup` 📖	mathematical	`Filter.IsBoundedUnder` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Filter.atTop` `Nat.instPreorder`	`linearGrowthInf` `linearGrowthSup`	—	`Filter.liminf_le_limsup` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat`
`linearGrowthInf_le_linearGrowthSup_of_frequently_le` 📖	mathematical	`Filter.Frequently` `EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `Filter.atTop` `Nat.instPreorder`	`linearGrowthInf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `linearGrowthSup`	—	`Filter.liminf_le_limsup_of_frequently_le` `Filter.isBounded_ge_of_bot` `Filter.isBounded_le_of_top` `Filter.Frequently.mono` `EReal.div_le_div_right_of_nonneg` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoidEReal` `instZeroLEOneClassEReal`
`linearGrowthInf_le_of_eventually_le` 📖	mathematical	`Filter.Eventually` `EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidEReal` `Filter.atTop` `Nat.instPreorder`	`linearGrowthInf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal`	—	`LE.le.trans` `linearGrowthInf_eventually_monotone` `eq_bot_or_bot_lt` `EReal.add_bot` `linearGrowthInf_bot` `LE.le.trans_eq` `linearGrowthInf_add_le'` `linearGrowthSup_const` `LT.lt.ne'` `EReal.zero_ne_top` `EReal.zero_ne_bot` `add_zero`
`linearGrowthInf_monotone` 📖	mathematical	`Pi.hasLe` `EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal`	`linearGrowthInf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal`	—	`linearGrowthInf_eventually_monotone` `Filter.Eventually.of_forall`
`linearGrowthInf_natCast_nonneg` 📖	mathematical	—	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal` `linearGrowthInf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal`	—	`Filter.le_liminf_of_le` `Filter.isCobounded_ge_of_top` `Filter.Eventually.of_forall` `EReal.div_nonneg` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoidEReal` `instZeroLEOneClassEReal`
`linearGrowthInf_neg` 📖	mathematical	—	`linearGrowthInf` `EReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `Pi.instNeg` `EReal.instNeg` `linearGrowthSup`	—	`linearGrowthSup.eq_1` `EReal.liminf_neg` `Filter.liminf_congr` `Filter.Eventually.of_forall` `Pi.neg_apply` `div_eq_mul_inv` `neg_mul`
`linearGrowthInf_top` 📖	mathematical	—	`linearGrowthInf` `EReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `Top.top` `Pi.instTopForall` `EReal.instTop`	—	`Filter.liminf_const` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Filter.liminf_congr` `Filter.eventually_atTop` `EReal.top_div_of_pos_ne_top` `Nat.cast_pos'` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoidEReal` `instZeroLEOneClassEReal` `NeZero.charZero_one` `instCharZeroEReal` `EReal.natCast_ne_top`
`linearGrowthInf_zero` 📖	mathematical	—	`linearGrowthInf` `EReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `Pi.instZero` `instZeroEReal`	—	`linearGrowthInf_const` `EReal.zero_ne_bot` `EReal.zero_ne_top`
`linearGrowthSup_add_le` 📖	mathematical	—	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `linearGrowthSup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidEReal`	—	`LE.le.trans_eq'` `EReal.limsup_add_le` `Filter.limsup_congr` `Filter.Eventually.of_forall` `Pi.add_apply` `EReal.add_div_of_nonneg_right` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoidEReal` `instZeroLEOneClassEReal`
`linearGrowthSup_biSup` 📖	mathematical	—	`linearGrowthSup` `EReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `iSup` `Pi.supSet` `instSupSetEReal` `Set` `Set.instMembership`	—	`map_finset_sup` `SupBotHom.instSupBotHomClass` `linearGrowthSup_sup` `linearGrowthSup_bot` `Finset.sup_eq_iSup` `iSup_congr_Prop` `Set.Finite.mem_toFinset`
`linearGrowthSup_bot` 📖	mathematical	—	`linearGrowthSup` `EReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `Bot.bot` `Pi.instBotForall` `instBotEReal`	—	`Filter.limsup_const` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Filter.limsup_congr` `Filter.Eventually.mono` `Filter.eventually_gt_atTop` `instNoTopOrderOfNoMaxOrder` `Nat.instNoMaxOrder` `EReal.bot_div_of_pos_ne_top` `Nat.cast_pos'` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoidEReal` `instZeroLEOneClassEReal` `NeZero.charZero_one` `instCharZeroEReal` `EReal.natCast_ne_top`
`linearGrowthSup_comp_le` 📖	mathematical	`Filter.Frequently` `EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal` `Filter.atTop` `Nat.instPreorder` `Filter.Tendsto`	`linearGrowthSup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `EReal.instMul`	—	`Ne.lt_of_le` `LE.le.trans` `linearGrowthInf_natCast_nonneg` `Filter.liminf_le_limsup` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Filter.isBounded_le_of_top` `Filter.isBounded_ge_of_bot` `EReal.le_mul_of_forall_lt` `Eventually.linearGrowthSup_le` `linearGrowthInf_const` `EReal.zero_ne_bot` `EReal.zero_ne_top` `linearGrowthInf_le_linearGrowthSup_of_frequently_le` `LT.lt.le` `Filter.eventually_map` `Filter.Eventually.filter_mono` `eventually_le_mul` `Filter.mp_mem` `Filter.eventually_gt_atTop` `instNoTopOrderOfNoMaxOrder` `Nat.instNoMaxOrder` `Filter.eventually_lt_of_limsup_lt` `Filter.univ_mem'` `EReal.div_lt_iff` `Nat.cast_pos'` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoidEReal` `instZeroLEOneClassEReal` `NeZero.charZero_one` `instCharZeroEReal` `EReal.natCast_ne_top` `mul_comm` `mul_assoc` `mul_le_mul_of_nonneg_left` `EReal.instPosMulMono`
`linearGrowthSup_comp_nonneg` 📖	mathematical	`Monotone` `EReal` `Nat.instPreorder` `PartialOrder.toPreorder` `instPartialOrderEReal` `Filter.Tendsto` `Filter.atTop`	`Preorder.toLE` `instZeroEReal` `linearGrowthSup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal`	—	`LE.le.trans` `linearGrowthInf_comp_nonneg` `linearGrowthInf_le_linearGrowthSup` `Filter.isBounded_le_of_top` `Filter.isBounded_ge_of_bot`
`linearGrowthSup_congr` 📖	mathematical	`Filter.EventuallyEq` `Filter.atTop` `Nat.instPreorder`	`linearGrowthSup`	—	`Filter.limsup_congr` `Filter.Eventually.mono`
`linearGrowthSup_const` 📖	mathematical	—	`linearGrowthSup` `EReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `instZeroEReal`	—	`Filter.Tendsto.limsup_eq` `EReal.instOrderTopology` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `EReal.tendsto_const_div_atTop_nhds_zero_nat`
`linearGrowthSup_const_mul_self` 📖	mathematical	—	`linearGrowthSup` `EReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `EReal.instMul`	—	`le_antisymm` `Eventually.linearGrowthSup_le` `Filter.Eventually.of_forall` `le_refl` `Frequently.le_linearGrowthSup` `Filter.Frequently.of_forall` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat`
`linearGrowthSup_eventually_monotone` 📖	mathematical	`Filter.EventuallyLE` `EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `Filter.atTop` `Nat.instPreorder`	`linearGrowthSup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal`	—	`Filter.limsup_le_limsup` `Filter.Eventually.mono` `EReal.monotone_div_right_of_nonneg` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoidEReal` `instZeroLEOneClassEReal` `Filter.isCobounded_le_of_bot` `Filter.isBounded_le_of_top`
`linearGrowthSup_iSup` 📖	mathematical	—	`linearGrowthSup` `EReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `iSup` `Pi.supSet` `instSupSetEReal`	—	`iSup_univ` `linearGrowthSup_biSup` `Set.finite_univ`
`linearGrowthSup_inv` 📖	mathematical	—	`linearGrowthSup` `EReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `Pi.instNeg` `EReal.instNeg` `linearGrowthInf`	—	`linearGrowthInf.eq_1` `EReal.limsup_neg` `Filter.limsup_congr` `Filter.Eventually.of_forall` `Pi.neg_apply` `div_eq_mul_inv` `neg_mul`
`linearGrowthSup_le_iff` 📖	mathematical	—	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `linearGrowthSup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `Filter.Eventually` `EReal.instMul` `Filter.atTop` `Nat.instPreorder`	—	`linearGrowthSup.eq_1` `Filter.limsup_le_iff'` `instDenselyOrderedEReal` `Filter.isCobounded_le_of_bot` `Filter.isBounded_le_of_top` `Filter.eventually_congr` `Filter.eventually_atTop` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `EReal.div_le_iff_le_mul` `Nat.cast_zero` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoidEReal` `instZeroLEOneClassEReal` `instCharZeroEReal` `EReal.natCast_ne_top` `mul_comm`
`linearGrowthSup_le_of_eventually_le` 📖	mathematical	`Filter.Eventually` `EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidEReal` `Filter.atTop` `Nat.instPreorder`	`linearGrowthSup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal`	—	`LE.le.trans` `linearGrowthSup_eventually_monotone` `eq_bot_or_bot_lt` `EReal.add_bot` `linearGrowthSup_bot` `LE.le.trans_eq` `linearGrowthSup_add_le` `linearGrowthSup_const` `LT.lt.ne'` `EReal.zero_ne_top` `EReal.zero_ne_bot` `add_zero`
`linearGrowthSup_monotone` 📖	mathematical	`Pi.hasLe` `EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal`	`linearGrowthSup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal`	—	`linearGrowthSup_eventually_monotone` `Filter.Eventually.of_forall`
`linearGrowthSup_sup` 📖	mathematical	—	`linearGrowthSup` `EReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `Pi.instMaxForall_mathlib` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice`	—	`linearGrowthSup.eq_1` `limsup_max` `Filter.isCobounded_le_of_bot` `Filter.isBounded_le_of_top` `Filter.limsup_congr` `Filter.Eventually.of_forall` `Monotone.map_max` `EReal.monotone_div_right_of_nonneg` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoidEReal` `instZeroLEOneClassEReal`
`linearGrowthSup_top` 📖	mathematical	—	`linearGrowthSup` `EReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `Top.top` `Pi.instTopForall` `EReal.instTop`	—	`top_le_iff` `linearGrowthInf_top` `linearGrowthInf_le_linearGrowthSup` `Filter.isBounded_le_of_top` `Filter.isBounded_ge_of_bot`
`linearGrowthSup_zero` 📖	mathematical	—	`linearGrowthSup` `EReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `Pi.instZero` `instZeroEReal`	—	`linearGrowthSup_const` `EReal.zero_ne_bot` `EReal.zero_ne_top`
`tendsto_atTop_of_linearGrowthInf_natCast_pos` 📖	mathematical	—	`Filter.Tendsto` `Filter.atTop` `Nat.instPreorder`	—	`Filter.tendsto_atTop` `tendsto_atTop_of_linearGrowthInf_pos` `Ne.lt_of_le'` `linearGrowthInf_natCast_nonneg` `Filter.Eventually.mono` `EReal.tendsto_nhds_top_iff_real` `EReal.coe_coe_eq_natCast` `Nat.cast_lt` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoidEReal` `instZeroLEOneClassEReal` `instCharZeroEReal` `le_of_lt`
`tendsto_atTop_of_linearGrowthInf_pos` 📖	mathematical	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal` `linearGrowthInf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal`	`Filter.Tendsto` `Filter.atTop` `Nat.instPreorder` `nhds` `EReal.instTopologicalSpace` `Top.top` `EReal.instTop`	—	`exists_between` `instDenselyOrderedEReal` `tendsto_nhds_top_mono` `EReal.instOrderTopology` `EReal.tendsto_nhds_top_iff_real` `Filter.eventually_atTop` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `CanLift.prf` `EReal.canLift` `ne_top_of_lt` `ne_bot_of_gt` `exists_nat_ge` `Real.instIsOrderedRing` `Real.instArchimedean` `EReal.coe_coe_eq_natCast` `EReal.coe_mul` `EReal.coe_lt_coe_iff` `mul_comm` `div_lt_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `EReal.coe_pos` `LE.le.trans_lt` `Nat.cast_lt` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `IsStrictOrderedRing.toCharZero` `le_linearGrowthInf_iff` `le_refl`

LinearGrowth.EReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eventually_atTop_exists_nat_between` 📖	mathematical	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `Preorder.toLE` `instZeroEReal`	`Filter.Eventually` `EReal.instMul` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `Filter.atTop` `Nat.instPreorder`	—	`not_top_lt` `Filter.Eventually.of_forall` `Nat.cast_zero` `EReal.mul_nonpos_iff` `bot_le` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoidEReal` `instZeroLEOneClassEReal` `mul_nonneg` `EReal.instPosMulMono` `Filter.Eventually.mono` `Filter.eventually_gt_atTop` `instNoTopOrderOfNoMaxOrder` `Nat.instNoMaxOrder` `EReal.exists_nat_ge_mul` `LT.lt.ne` `le_top` `EReal.top_mul_of_pos` `Nat.cast_pos'` `NeZero.charZero_one` `instCharZeroEReal` `not_lt_bot` `Filter.eventually_atTop` `instIsDirectedOrder` `Real.instIsOrderedRing` `Real.instArchimedean` `LinearGrowth.Real.eventually_atTop_exists_nat_between` `EReal.coe_lt_coe_iff` `EReal.coe_nonneg` `exists_nat_ge` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `LE.le.trans` `Nat.cast_le` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing`

LinearGrowth.Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eventually_atTop_exists_int_between` 📖	mathematical	`Real` `Real.instLT`	`Filter.Eventually` `Real.instLE` `Real.instMul` `Real.instIntCast` `Filter.atTop` `Real.instPreorder`	—	`Filter.Eventually.mono` `Filter.eventually_ge_atTop` `le_of_add_le_add_right` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `LE.le.trans` `le_sub_iff_add_le'` `sub_mul` `mul_comm` `inv_le_iff_one_le_mul₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `sub_pos_of_lt` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `covariant_swap_add_of_covariant_add` `LT.lt.le` `Int.lt_floor_add_one` `Int.floor_le`
`eventually_atTop_exists_nat_between` 📖	mathematical	`Real` `Real.instLT` `Real.instLE` `Real.instZero`	`Filter.Eventually` `Real.instMul` `Real.instNatCast` `Filter.atTop` `Real.instPreorder`	—	`Filter.mp_mem` `eventually_atTop_exists_int_between` `Filter.eventually_ge_atTop` `Filter.univ_mem'` `LE.le.trans` `Int.cast_le` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `Nat.cast_zero` `Int.cast_zero` `Int.cast_natCast` `max_le` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing`

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_linearGrowthSup_comp` 📖	mathematical	`Monotone` `EReal` `Nat.instPreorder` `PartialOrder.toPreorder` `instPartialOrderEReal`	`Preorder.toLE` `EReal.instMul` `LinearGrowth.linearGrowthInf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `LinearGrowth.linearGrowthSup`	—	`Ne.lt_of_le` `LinearGrowth.linearGrowthInf_natCast_nonneg` `LinearGrowth.linearGrowthSup_bot` `EReal.mul_bot_of_pos` `bot_le` `EReal.mul_le_of_forall_lt_of_nonneg` `LT.lt.le` `LinearGrowth.linearGrowthSup_comp_nonneg` `LinearGrowth.tendsto_atTop_of_linearGrowthInf_natCast_pos` `Frequently.le_linearGrowthSup` `exists_between` `instDenselyOrderedEReal` `ne_top_of_lt` `LT.lt.trans` `EReal.inv_strictAntiOn` `Set.mem_Ioi` `Filter.mp_mem` `Filter.eventually_gt_atTop` `instNoTopOrderOfNoMaxOrder` `Nat.instNoMaxOrder` `Filter.eventually_lt_of_lt_liminf` `Filter.isBounded_ge_of_bot` `Filter.univ_mem'` `EReal.le_div_iff_mul_le` `Nat.cast_pos'` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoidEReal` `instZeroLEOneClassEReal` `NeZero.charZero_one` `instCharZeroEReal` `EReal.natCast_ne_top` `Filter.frequently_imp_distrib` `Filter.Frequently.and_eventually` `LinearGrowth.frequently_mul_le` `LinearGrowth.EReal.eventually_atTop_exists_nat_between` `EReal.inv_nonneg_of_nonneg` `Filter.frequently_atTop` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `EReal.exists_nat_ge_mul` `Nat.cast_le` `LE.le.trans` `EReal.div_eq_inv_mul` `mul_comm` `LE.le.trans'` `mul_le_mul_of_nonneg_left` `EReal.instPosMulMono` `Nat.mono_cast` `le_of_lt` `mul_assoc` `EReal.div_le_iff_le_mul` `le_trans`
`linearGrowthInf_comp` 📖	mathematical	`Monotone` `EReal` `Nat.instPreorder` `PartialOrder.toPreorder` `instPartialOrderEReal` `Filter.Tendsto` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `Filter.atTop` `nhds` `EReal.instTopologicalSpace`	`LinearGrowth.linearGrowthInf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `EReal.instMul`	—	`Ne.lt_of_le` `Filter.Tendsto.liminf_eq` `EReal.instOrderTopology` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `LinearGrowth.linearGrowthInf_natCast_nonneg` `LinearGrowth.tendsto_atTop_of_linearGrowthInf_natCast_pos` `LT.lt.ne` `Pi.bot_comp` `LinearGrowth.linearGrowthInf_bot` `EReal.mul_bot_of_pos` `Filter.frequently_atTop` `LE.le.trans` `le_antisymm` `LE.le.trans_eq` `LinearGrowth.linearGrowthInf_monotone` `LinearGrowth.linearGrowthInf_const` `EReal.zero_ne_bot` `EReal.zero_ne_top` `linearGrowthInf_nonneg` `MulZeroClass.mul_zero` `LinearGrowth.linearGrowthInf_comp_nonneg` `Filter.Eventually.mono` `LT.lt.le` `Filter.Tendsto.limsup_eq` `linearGrowthInf_comp_le` `LinearGrowth.le_linearGrowthInf_comp`
`linearGrowthInf_comp_le` 📖	mathematical	`Monotone` `EReal` `Nat.instPreorder` `PartialOrder.toPreorder` `instPartialOrderEReal`	`Preorder.toLE` `LinearGrowth.linearGrowthInf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `EReal.instMul` `LinearGrowth.linearGrowthSup`	—	`Pi.bot_comp` `LinearGrowth.linearGrowthInf_bot` `bot_le` `Ne.lt_of_le` `LE.le.trans` `LinearGrowth.linearGrowthInf_natCast_nonneg` `Filter.liminf_le_limsup` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Filter.isBounded_le_of_top` `Filter.isBounded_ge_of_bot` `EReal.le_mul_of_forall_lt` `LT.lt.trans` `LE.le.trans_lt` `linearGrowthInf_nonneg` `eq_or_ne` `EReal.top_mul_of_pos` `le_top` `Frequently.linearGrowthInf_le` `exists_between` `instDenselyOrderedEReal` `EReal.inv_strictAntiOn` `Set.mem_Ioi` `Filter.mp_mem` `Filter.eventually_gt_atTop` `instNoTopOrderOfNoMaxOrder` `Nat.instNoMaxOrder` `Filter.eventually_lt_of_limsup_lt` `Filter.univ_mem'` `mul_comm` `EReal.div_le_iff_le_mul` `Nat.cast_pos'` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoidEReal` `instZeroLEOneClassEReal` `NeZero.charZero_one` `instCharZeroEReal` `EReal.natCast_ne_top` `LT.lt.le` `Filter.frequently_imp_distrib` `Filter.Frequently.and_eventually` `LinearGrowth.frequently_le_mul` `LinearGrowth.EReal.eventually_atTop_exists_nat_between` `EReal.inv_nonneg_of_nonneg` `Filter.frequently_atTop` `EReal.exists_nat_ge_mul` `Nat.cast_le` `EReal.div_eq_inv_mul` `EReal.le_div_iff_mul_le` `LE.le.trans'` `mul_le_mul_of_nonneg_left` `EReal.instPosMulMono` `Nat.mono_cast` `le_of_lt` `mul_assoc` `ne_top_of_lt`
`linearGrowthInf_comp_mul` 📖	mathematical	`Monotone` `EReal` `Nat.instPreorder` `PartialOrder.toPreorder` `instPartialOrderEReal`	`LinearGrowth.linearGrowthInf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `EReal.instMul`	—	`tendsto_nhds_of_eventually_eq` `Filter.Eventually.mono` `Filter.eventually_gt_atTop` `instNoTopOrderOfNoMaxOrder` `Nat.instNoMaxOrder` `mul_comm` `EReal.natCast_mul` `EReal.mul_div` `EReal.mul_div_cancel` `EReal.natCast_ne_bot` `EReal.natCast_ne_top` `Nat.cast_ne_zero` `instCharZeroEReal` `LT.lt.ne` `linearGrowthInf_comp`
`linearGrowthInf_nonneg` 📖	mathematical	`Monotone` `EReal` `Nat.instPreorder` `PartialOrder.toPreorder` `instPartialOrderEReal`	`Preorder.toLE` `instZeroEReal` `LinearGrowth.linearGrowthInf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal`	—	`Filter.eventually_atTop` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `eq_or_ne` `LE.le.trans` `le_top` `Eq.trans_le` `LinearGrowth.linearGrowthInf_top` `LinearGrowth.linearGrowthInf_eventually_monotone` `LinearGrowth.linearGrowthInf_const`
`linearGrowthSup_comp` 📖	mathematical	`Monotone` `EReal` `Nat.instPreorder` `PartialOrder.toPreorder` `instPartialOrderEReal` `Filter.Tendsto` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `Filter.atTop` `nhds` `EReal.instTopologicalSpace`	`LinearGrowth.linearGrowthSup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `EReal.instMul`	—	`Ne.lt_of_le` `Filter.Tendsto.liminf_eq` `EReal.instOrderTopology` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `LinearGrowth.linearGrowthInf_natCast_nonneg` `LinearGrowth.tendsto_atTop_of_linearGrowthInf_natCast_pos` `LT.lt.ne` `Pi.bot_comp` `LinearGrowth.linearGrowthSup_bot` `EReal.mul_bot_of_pos` `le_antisymm` `LE.le.trans_eq` `LinearGrowth.linearGrowthSup_eventually_monotone` `LinearGrowth.linearGrowthSup_const` `EReal.zero_ne_bot` `EReal.zero_ne_top` `linearGrowthSup_nonneg` `MulZeroClass.mul_zero` `Filter.Tendsto.eventually` `LinearGrowth.linearGrowthSup_comp_nonneg` `Filter.Frequently.mono` `LT.lt.le` `Filter.Tendsto.limsup_eq` `LinearGrowth.linearGrowthSup_comp_le` `le_linearGrowthSup_comp`
`linearGrowthSup_comp_mul` 📖	mathematical	`Monotone` `EReal` `Nat.instPreorder` `PartialOrder.toPreorder` `instPartialOrderEReal`	`LinearGrowth.linearGrowthSup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `EReal.instMul`	—	`tendsto_nhds_of_eventually_eq` `Filter.Eventually.mono` `Filter.eventually_gt_atTop` `instNoTopOrderOfNoMaxOrder` `Nat.instNoMaxOrder` `mul_comm` `EReal.natCast_mul` `EReal.mul_div` `EReal.mul_div_cancel` `EReal.natCast_ne_bot` `EReal.natCast_ne_top` `Nat.cast_ne_zero` `instCharZeroEReal` `LT.lt.ne` `linearGrowthSup_comp`
`linearGrowthSup_nonneg` 📖	mathematical	`Monotone` `EReal` `Nat.instPreorder` `PartialOrder.toPreorder` `instPartialOrderEReal`	`Preorder.toLE` `instZeroEReal` `LinearGrowth.linearGrowthSup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `DivInvMonoid.toDiv` `EReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal`	—	`LE.le.trans` `linearGrowthInf_nonneg` `LinearGrowth.linearGrowthInf_le_linearGrowthSup` `Filter.isBounded_le_of_top` `Filter.isBounded_ge_of_bot`

---

← Back to Index