α : Type u_1
β : Type ?u.67098
γ : Type ?u.67101
ι : Sort ?u.67104
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
a b : α
hs : Set.Nonempty s
hb : ∀ (a : α), a ∈ s → a ≤ b
⊢ sSup s ≤ b
α : Type u_1
β : Type ?u.67098
γ : Type ?u.67101
ι : Sort ?u.67104
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
a b : α
hs : Set.Nonempty s
hb : b < sSup s
⊢ ∃ a, a ∈ s ∧ b < a
contrapose! hb
no goals
α : Type u_1
β : Type ?u.67098
γ : Type ?u.67101
ι : Sort ?u.67104
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
a b : α
hs : Set.Nonempty s
hb : ∀ (a : α), a ∈ s → a ≤ b
⊢ sSup s ≤ b
exact csSup_le hs hb