Lower bounds of 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-03-13.

module elementary-number-theory.lower-bounds-natural-numbers where
open import elementary-number-theory.inequality-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.dependent-pair-types
open import foundation.propositions
open import foundation.universe-levels


A lower bound for a type family P over the natural numbers is a natural number n such that P x → n ≤ x for all x : ℕ.


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


Being a lower bound is a property

module _
  {l1 : Level} {P :   UU l1}

    is-prop-is-lower-bound-ℕ : (x : )  is-prop (is-lower-bound-ℕ P x)
    is-prop-is-lower-bound-ℕ x =
      is-prop-Π  y  is-prop-function-type (is-prop-leq-ℕ x y))

  is-lower-bound-ℕ-Prop : (x : )  Prop l1
  pr1 (is-lower-bound-ℕ-Prop x) = is-lower-bound-ℕ P x
  pr2 (is-lower-bound-ℕ-Prop x) = is-prop-is-lower-bound-ℕ x

Recent changes