constructor
X : Type u_1
inst✝ : PartialOrder X
I : Set X → X
h : isInfFun I
s : Set X
x : X
⊢ x ∈ upperBounds s ↔ (fun s => I (upperBounds s)) s ≤ x
case mp
X : Type u_1
inst✝ : PartialOrder X
I : Set X → X
h : isInfFun I
s : Set X
x : X
⊢ x ∈ upperBounds s → (fun s => I (upperBounds s)) s ≤ x

case mpr
X : Type u_1
inst✝ : PartialOrder X
I : Set X → X
h : isInfFun I
s : Set X
x : X
⊢ (fun s => I (upperBounds s)) s ≤ x → x ∈ upperBounds s