Upper bounds of chains in posets

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2024-10-20.
Last modified on 2024-11-20.

module order-theory.upper-bounds-chains-posets where
Imports 
open import foundation.existential-quantification
open import foundation.universe-levels

open import foundation-core.function-types
open import foundation-core.propositions

open import order-theory.chains-posets
open import order-theory.posets
open import order-theory.upper-bounds-posets

Idea

An upper bound on a chain C in a poset P is an element x such that for every element y in C, y ≤ x holds.

Definition

module _
  {l1 l2 l3 : Level} (X : Poset l1 l2) (C : chain-Poset l3 X)
  where

  is-upper-bound-chain-prop-Poset : type-Poset X → Prop (l1 ⊔ l2 ⊔ l3)
  is-upper-bound-chain-prop-Poset =
    is-upper-bound-family-of-elements-prop-Poset X
      ( inclusion-type-chain-Poset X C)

  is-upper-bound-chain-Poset : type-Poset X → UU (l1 ⊔ l2 ⊔ l3)
  is-upper-bound-chain-Poset = type-Prop ∘ is-upper-bound-chain-prop-Poset

  has-upper-bound-chain-prop-Poset : Prop (l1 ⊔ l2 ⊔ l3)
  has-upper-bound-chain-prop-Poset =
    ∃ (type-Poset X) is-upper-bound-chain-prop-Poset

  has-upper-bound-chain-Poset : UU (l1 ⊔ l2 ⊔ l3)
  has-upper-bound-chain-Poset = type-Prop has-upper-bound-chain-prop-Poset

Recent changes