constructor
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
⊢ t ∈ upperBounds S ↔ ⋃₀ S ≤ t
case mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
⊢ t ∈ upperBounds S → ⋃₀ S ≤ t

case mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
⊢ ⋃₀ S ≤ t → t ∈ upperBounds S