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