# Lower bounds in posets

```agda
module order-theory.lower-bounds-posets where
```

<details><summary>Imports</summary>

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

open import order-theory.posets
```

</details>

## Idea

A **lower bound** of two elements `a` and `b` in a poset `P` is an element `x`
such that both `x ≤ a` and `x ≤ b` hold. Similarly, a **lower bound** of a
family `a : I → P` of elements in `P` is an element `x` such that `x ≤ a i`
holds for every `i : I`.

## Definitions

### Binary lower bounds

```agda
module _
  {l1 l2 : Level} (P : Poset l1 l2) (a b x : type-Poset P)
  where

  is-binary-lower-bound-Poset-Prop : Prop l2
  is-binary-lower-bound-Poset-Prop =
    product-Prop (leq-Poset-Prop P x a) (leq-Poset-Prop P x b)

  is-binary-lower-bound-Poset : UU l2
  is-binary-lower-bound-Poset =
    type-Prop is-binary-lower-bound-Poset-Prop

  is-prop-is-binary-lower-bound-Poset : is-prop is-binary-lower-bound-Poset
  is-prop-is-binary-lower-bound-Poset =
    is-prop-type-Prop is-binary-lower-bound-Poset-Prop

module _
  {l1 l2 : Level} (P : Poset l1 l2) {a b x : type-Poset P}
  (H : is-binary-lower-bound-Poset P a b x)
  where

  leq-left-is-binary-lower-bound-Poset : leq-Poset P x a
  leq-left-is-binary-lower-bound-Poset = pr1 H

  leq-right-is-binary-lower-bound-Poset : leq-Poset P x b
  leq-right-is-binary-lower-bound-Poset = pr2 H
```

### Lower bounds of families of elements

```agda
module _
  {l1 l2 l3 : Level} (P : Poset l1 l2) {I : UU l3} (x : I → type-Poset P)
  where

  is-lower-bound-family-of-elements-Poset-Prop : type-Poset P → Prop (l2 ⊔ l3)
  is-lower-bound-family-of-elements-Poset-Prop z =
    Π-Prop I (λ i → leq-Poset-Prop P z (x i))

  is-lower-bound-family-of-elements-Poset : type-Poset P → UU (l2 ⊔ l3)
  is-lower-bound-family-of-elements-Poset z =
    type-Prop (is-lower-bound-family-of-elements-Poset-Prop z)

  is-prop-is-lower-bound-family-of-elements-Poset :
    (z : type-Poset P) → is-prop (is-lower-bound-family-of-elements-Poset z)
  is-prop-is-lower-bound-family-of-elements-Poset z =
    is-prop-type-Prop (is-lower-bound-family-of-elements-Poset-Prop z)
```

## Properties

### Any element less than a lower bound of `a` and `b` is a lower bound of `a` and `b`

```agda
module _
  {l1 l2 : Level} (P : Poset l1 l2) {a b x : type-Poset P}
  (H : is-binary-lower-bound-Poset P a b x)
  where

  is-binary-lower-bound-leq-Poset :
    {y : type-Poset P} →
    leq-Poset P y x → is-binary-lower-bound-Poset P a b y
  pr1 (is-binary-lower-bound-leq-Poset K) =
    transitive-leq-Poset P _ x a
      ( leq-left-is-binary-lower-bound-Poset P H)
      ( K)
  pr2 (is-binary-lower-bound-leq-Poset K) =
    transitive-leq-Poset P _ x b
      ( leq-right-is-binary-lower-bound-Poset P H)
      ( K)
```

### Any element less than a lower bound of a family of elements `a` is a lower bound of `a`

```agda
module _
  {l1 l2 l3 : Level} (P : Poset l1 l2) {I : UU l3} {a : I → type-Poset P}
  {x : type-Poset P} (H : is-lower-bound-family-of-elements-Poset P a x)
  where

  is-lower-bound-family-of-elements-leq-Poset :
    {y : type-Poset P} → leq-Poset P y x →
    is-lower-bound-family-of-elements-Poset P a y
  is-lower-bound-family-of-elements-leq-Poset K i =
    transitive-leq-Poset P _ x (a i) (H i) K
```