# Upper sets of large posets

Content created by Egbert Rijke.

Created on 2023-11-24.
Last modified on 2023-11-24.

module order-theory.upper-sets-large-posets where

Imports
open import foundation.universe-levels

open import order-theory.large-posets
open import order-theory.large-subposets


## Idea

An upper set or upwards closed set in a large poset is a large subposet that is upwards closed, i.e., that satisfies the condition that

  ∀ (x y : P), (x ≤ y) → x ∈ S → y ∈ S.


## Definitions

### The predicate of being an upper set

module _
{α γ : Level → Level} {β : Level → Level → Level}
(P : Large-Poset α β) (S : Large-Subposet γ P)
where

is-upper-set-Large-Subposet : UUω
is-upper-set-Large-Subposet =
{l1 l2 : Level} (x : type-Large-Poset P l1) (y : type-Large-Poset P l2) →
leq-Large-Poset P x y →
is-in-Large-Subposet P S x → is-in-Large-Subposet P S y


### Upper sets of a large poset

module _
{α : Level → Level} {β : Level → Level → Level} (γ : Level → Level)
(P : Large-Poset α β)
where

record
upper-set-Large-Poset : UUω
where
field
large-subposet-upper-set-Large-Poset :
Large-Subposet γ P
is-upper-set-upper-set-Large-Poset :
is-upper-set-Large-Subposet P large-subposet-upper-set-Large-Poset

open upper-set-Large-Poset public