α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t : Set α
a b : α
inst✝ : SemilatticeSup γ
s : Set γ
x₀ : γ
⊢ Monotone fun x => ∀ (y : γ), y ∈ s → y ≤ x
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t : Set α
a b : α
inst✝ : SemilatticeSup γ
s : Set γ
x₀ : γ
⊢ BddAbove s ↔ ∃ x, x₀ ≤ x ∧ ∀ (y : γ), y ∈ s → y ≤ x
rw [bddAbove_def, exists_ge_and_iff_exists]
no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t : Set α
a b : α
inst✝ : SemilatticeSup γ
s : Set γ
x₀ : γ
⊢ Monotone fun x => ∀ (y : γ), y ∈ s → y ≤ x
exact Monotone.ball fun x _ => monotone_le