# Upper bounds in large posets

Content created by Egbert Rijke, Fredrik Bakke and Gregor Perčič.

Created on 2023-05-09.

module order-theory.upper-bounds-large-posets where
Imports
open import foundation.dependent-pair-types
open import foundation.logical-equivalences
open import foundation.propositions
open import foundation.universe-levels

open import order-theory.dependent-products-large-posets
open import order-theory.large-posets

## Idea

A binary upper bound of two elements a and b of a large poset P is an element x of P such that a ≤ x and b ≤ x both hold. Similarly, an upper bound of a family a : I → P of elements of P is an element x of P such that the inequality (a i) ≤ x holds for every i : I.

## Definitions

### The predicate of being an upper bound of a family of elements

module _
{α : Level  Level} {β : Level  Level  Level}
(P : Large-Poset α β)
{l1 l2 : Level} {I : UU l1} (x : I  type-Large-Poset P l2)
where

is-upper-bound-prop-family-of-elements-Large-Poset :
{l3 : Level} (y : type-Large-Poset P l3)  Prop (β l2 l3  l1)
is-upper-bound-prop-family-of-elements-Large-Poset y =
Π-Prop I  i  leq-prop-Large-Poset P (x i) y)

is-upper-bound-family-of-elements-Large-Poset :
{l3 : Level} (y : type-Large-Poset P l3)  UU (β l2 l3  l1)
is-upper-bound-family-of-elements-Large-Poset y =
type-Prop (is-upper-bound-prop-family-of-elements-Large-Poset y)

is-prop-is-upper-bound-family-of-elements-Large-Poset :
{l3 : Level} (y : type-Large-Poset P l3)
is-prop (is-upper-bound-family-of-elements-Large-Poset y)
is-prop-is-upper-bound-family-of-elements-Large-Poset y =
is-prop-type-Prop (is-upper-bound-prop-family-of-elements-Large-Poset y)

## Properties

### An element x : Π-Large-Poset P of a dependent product of large posets P i indexed by i : I is an upper bound of a family a : J → Π-Large-Poset P if and only if x i is an upper bound of the family (j ↦ a j i) : J → P i of elements of P i

module _
{α : Level  Level} {β : Level  Level  Level}
{l1 : Level} {I : UU l1} (P : I  Large-Poset α β)
{l2 l3 : Level} {J : UU l2} (a : J  type-Π-Large-Poset P l3)
{l4 : Level} (x : type-Π-Large-Poset P l4)
where

is-upper-bound-family-of-elements-Π-Large-Poset :
( (i : I)
is-upper-bound-family-of-elements-Large-Poset (P i)  j  a j i) (x i))
is-upper-bound-family-of-elements-Large-Poset (Π-Large-Poset P) a x
is-upper-bound-family-of-elements-Π-Large-Poset H j i = H i j

map-inv-is-upper-bound-family-of-elements-Π-Large-Poset :
is-upper-bound-family-of-elements-Large-Poset (Π-Large-Poset P) a x
(i : I)
is-upper-bound-family-of-elements-Large-Poset (P i)  j  a j i) (x i)
map-inv-is-upper-bound-family-of-elements-Π-Large-Poset H i j = H j i

logical-equivalence-is-upper-bound-family-of-elements-Π-Large-Poset :
( (i : I)
is-upper-bound-family-of-elements-Large-Poset (P i)  j  a j i) (x i))
is-upper-bound-family-of-elements-Large-Poset (Π-Large-Poset P) a x
pr1 logical-equivalence-is-upper-bound-family-of-elements-Π-Large-Poset =
is-upper-bound-family-of-elements-Π-Large-Poset
pr2 logical-equivalence-is-upper-bound-family-of-elements-Π-Large-Poset =
map-inv-is-upper-bound-family-of-elements-Π-Large-Poset