case pos
α : Type u_1
β : Type ?u.92784
γ : Type ?u.92787
ι : Sort ?u.92790
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : BddBelow s
⊢ IsGLB s (sInf s)

case neg
α : Type u_1
β : Type ?u.92784
γ : Type ?u.92787
ι : Sort ?u.92790
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : ¬BddBelow s
⊢ IsGLB s (sInf s)
α : Type u_1
β : Type ?u.92784
γ : Type ?u.92787
ι : Sort ?u.92790
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
⊢ IsGLB s (sInf s)
by_cases hs : BddBelow s
no goals
case pos
α : Type u_1
β : Type ?u.92784
γ : Type ?u.92787
ι : Sort ?u.92790
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : BddBelow s
⊢ IsGLB s (sInf s)
exact isGLB_sInf' hs
case neg.h
α : Type u_1
β : Type ?u.92784
γ : Type ?u.92787
ι : Sort ?u.92790
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : ¬BddBelow s
⊢ False
case neg
α : Type u_1
β : Type ?u.92784
γ : Type ?u.92787
ι : Sort ?u.92790
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : ¬BddBelow s
⊢ IsGLB s (sInf s)
exfalso
case neg.h
α : Type u_1
β : Type ?u.92784
γ : Type ?u.92787
ι : Sort ?u.92790
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : ¬BddBelow s
⊢ BddBelow s
case neg.h
α : Type u_1
β : Type ?u.92784
γ : Type ?u.92787
ι : Sort ?u.92790
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : ¬BddBelow s
⊢ False
apply hs
case neg.h
α : Type u_1
β : Type ?u.92784
γ : Type ?u.92787
ι : Sort ?u.92790
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : ¬BddBelow s
⊢ ⊥ ∈ lowerBounds s
case neg.h
α : Type u_1
β : Type ?u.92784
γ : Type ?u.92787
ι : Sort ?u.92790
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : ¬BddBelow s
⊢ BddBelow s
use ⊥
case neg.h
α : Type u_1
β : Type ?u.92784
γ : Type ?u.92787
ι : Sort ?u.92790
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : ¬BddBelow s
a✝¹ : WithTop α
a✝ : a✝¹ ∈ s
⊢ ⊥ ≤ a✝¹
case neg.h
α : Type u_1
β : Type ?u.92784
γ : Type ?u.92787
ι : Sort ?u.92790
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : ¬BddBelow s
⊢ ⊥ ∈ lowerBounds s
intro _ _
no goals
case neg.h
α : Type u_1
β : Type ?u.92784
γ : Type ?u.92787
ι : Sort ?u.92790
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : ¬BddBelow s
a✝¹ : WithTop α
a✝ : a✝¹ ∈ s
⊢ ⊥ ≤ a✝¹
exact bot_le