constructor
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
⊢ x' ∈ lowerBounds {x' | x ≤ x'} ↔ x' ≤ x
case mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
⊢ x' ∈ lowerBounds {x' | x ≤ x'} → x' ≤ x

case mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
⊢ x' ≤ x → x' ∈ lowerBounds {x' | x ≤ x'}