intro t
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
⊢ isInf S (⋂₀ S)
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
⊢ t ∈ lowerBounds S ↔ t ≤ ⋂₀ S