Mathlib Map

Theorems · Theorem · approximation theory

ExpGrowth.expGrowthSup_sup

∀ {u v : ℕ → ENNReal}, ExpGrowth.expGrowthSup (u ⊔ v) = max (ExpGrowth.expGrowthSup u) (ExpGrowth.expGrowthSup v)
Defined in
Mathlib.Analysis.Asymptotics.ExpGrowth
Cited by
2 results in Mathlib
Foundations
Depth 176 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.

ExpGrowth.expGrowthSup_add · cited by 2ExpGrowth.expGrowthSup_addExpGrowth.expGrowthSupBotHom · cited by 1ExpGrowth.expGrowthSupBot…ExpGrowth.expGrowthSup_biSup · cited by 1ExpGrowth.expGrowthSup_bi…ENNReal · cited by 9879ENNRealFilter.atTop · cited by 2405Filter.atTopEReal · cited by 793ERealFilter.Eventually.of_forall · cited by 526Eventually.of_forallNat.cast_nonneg' · cited by 245Nat.cast_nonneg'Filter.limsup · cited by 226Filter.limsupFilter.isBounded_le_of_top · cited by 75Filter.isBounded_le_of_topENNReal.log · cited by 72ENNReal.logFilter.isCobounded_le_of_bot · cited by 58Filter.isCobounded_le_of_…Monotone.map_max · cited by 55Monotone.map_maxExpGrowth.expGrowthSup · cited by 42ExpGrowth.expGrowthSupFilter.limsup_congr · cited by 20Filter.limsup_congrENNReal.log_monotone · cited by 14ENNReal.log_monotoneEReal.monotone_div_right_of_nonneg · cited by 11EReal.monotone_div_right_…limsup_max · cited by 3limsup_maxExpGrowth.expGrowthSup_supCITED BYCITES

Cites16

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

Cited by3

Results whose statement or proof uses this declaration.