Upper bounds for type families over the natural numbers

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

Created on 2022-02-14.
Last modified on 2023-04-08.

module elementary-number-theory.upper-bounds-natural-numbers where
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


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 : ℕ. Similar for strict upper bounds.


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


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