Upper bounds for type families over the natural numbers

Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke and Louis Wasserman.

Created on 2022-02-14.
Last modified on 2025-10-14.

module elementary-number-theory.upper-bounds-natural-numbers where
Imports 
open import elementary-number-theory.inequality-natural-numbers
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.strict-inequality-natural-numbers

open import foundation.universe-levels

Idea

A type family over the natural numbers has an upper bound n, if there is a function from P x to the type x ≤ n for all x : ℕ. Analogously, a strict upper bound is defined by a function from P x to the type x < n for all x : ℕ.

Definition

Upper bounds

is-upper-bound-ℕ :
  {l : Level} (P : ℕ → UU l) (n : ℕ) → UU l
is-upper-bound-ℕ P n =
  (m : ℕ) → P m → leq-ℕ m n

Strict upper bounds

is-strict-upper-bound-ℕ :
  {l : Level} (P : ℕ → UU l) (n : ℕ) → UU l
is-strict-upper-bound-ℕ P n =
  (m : ℕ) → P m → le-ℕ m n

Properties

A strict upper bound is an upper bound

is-upper-bound-is-strict-upper-bound-ℕ :
  {l : Level} (P : ℕ → UU l) (n : ℕ) →
  is-strict-upper-bound-ℕ P n → is-upper-bound-ℕ P n
is-upper-bound-is-strict-upper-bound-ℕ P n H x p =
  leq-le-ℕ x n (H x p)

Recent changes