α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
a b : α
h : IsGLB s a
⊢ b ≤ a ↔ b ∈ Iic a
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
a b : α
h : IsGLB s a
⊢ b ≤ a ↔ b ∈ lowerBounds s
rw [h.lowerBounds_eq]
no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
a b : α
h : IsGLB s a
⊢ b ≤ a ↔ b ∈ Iic a
rfl