Bounding number

DefinitionUnbounded family#✓fully proved

A family \(F\) of functions \(\mathbb{N} \to \mathbb{N}\) is unbounded if no function \(g : \mathbb{N} \to \mathbb{N}\) bounds every member of \(F\), where \(g\) bounds \(f\) if there is an \(N\) such that \(f(n) \le g(n)\) for all \(n \ge N\).

def IsUnboundedFamily (F : Set (ℕ → ℕ)) : Prop :=
  ¬ ∃ g : ℕ → ℕ, ∀ f ∈ F, f ≤ᶠ[Filter.atTop] g

Used by 1

Used byBounding number

DefinitionBounding number#✓fully proved

The bounding number \(\mathfrak{b}\) is the infimum of the cardinalities of all unbounded families of functions \(\mathbb{N} \to \mathbb{N}\).

noncomputable def boundingNumber : Cardinal :=
  sInf {c : Cardinal | ∃ F : Set (ℕ → ℕ), IsUnboundedFamily F ∧ #F = c}

Uses 1

Statement usesUnbounded family

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.