Theorems · Theorem · approximation theory

LinearGrowth.linearGrowthInf_le_linearGrowthSup

∀ {R : Type u_1} [inst : ConditionallyCompleteLattice R] [inst_1 : Div R] [inst_2 : NatCast R] {u : ℕ → R},
  autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) Filter.atTop fun n => u n / ↑n)
      LinearGrowth.linearGrowthInf_le_linearGrowthSup._auto_1 →
    autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) Filter.atTop fun n => u n / ↑n)
        LinearGrowth.linearGrowthInf_le_linearGrowthSup._auto_3 →
      LinearGrowth.linearGrowthInf u ≤ LinearGrowth.linearGrowthSup u

Defined in

Mathlib.Analysis.Asymptotics.LinearGrowth

Cited by

4 results in Mathlib

Foundations

Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

ConditionallyCompleteLatticeDivNatCast