case inl
α : Type u_1
β : Type ?u.73093
γ : Type ?u.73096
ι : Sort ?u.73099
inst✝ : ConditionallyCompleteLinearOrderBot α
hs : BddAbove ∅
⊢ IsLUB ∅ (sSup ∅)

case inr
α : Type u_1
β : Type ?u.73093
γ : Type ?u.73096
ι : Sort ?u.73099
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : BddAbove s
hne : Set.Nonempty s
⊢ IsLUB s (sSup s)
α : Type u_1
β : Type ?u.73093
γ : Type ?u.73096
ι : Sort ?u.73099
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : BddAbove s
⊢ IsLUB s (sSup s)
rcases eq_empty_or_nonempty s with (rfl | hne)
no goals
case inl
α : Type u_1
β : Type ?u.73093
γ : Type ?u.73096
ι : Sort ?u.73099
inst✝ : ConditionallyCompleteLinearOrderBot α
hs : BddAbove ∅
⊢ IsLUB ∅ (sSup ∅)
simp only [csSup_empty, isLUB_empty]
no goals
case inr
α : Type u_1
β : Type ?u.73093
γ : Type ?u.73096
ι : Sort ?u.73099
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : BddAbove s
hne : Set.Nonempty s
⊢ IsLUB s (sSup s)
exact isLUB_csSup hne hs