# 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.

module elementary-number-theory.lower-bounds-natural-numbers where

Imports
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


## Idea

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 : ℕ.

## Definition

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


## Properties

### Being a lower bound is a property

module _
{l1 : Level} {P : ℕ → UU l1}
where

abstract
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