case inl
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderClosedTopology α
f g : β → α
inst✝¹ : Nonempty α
inst✝ : TopologicalSpace β
s : Set α
hs : IsCompact s
h : OrderBot α
⊢ BddBelow s

case inr
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderClosedTopology α
f g : β → α
inst✝¹ : Nonempty α
inst✝ : TopologicalSpace β
s : Set α
hs : IsCompact s
h : NoBotOrder α
⊢ BddBelow s
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderClosedTopology α
f g : β → α
inst✝¹ : Nonempty α
inst✝ : TopologicalSpace β
s : Set α
hs : IsCompact s
⊢ BddBelow s
cases' botOrderOrNoBotOrder α with h h
case inr
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderClosedTopology α
f g : β → α
inst✝¹ : Nonempty α
inst✝ : TopologicalSpace β
s : Set α
hs : IsCompact s
h : NoBotOrder α
⊢ BddBelow s
case inl
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderClosedTopology α
f g : β → α
inst✝¹ : Nonempty α
inst✝ : TopologicalSpace β
s : Set α
hs : IsCompact s
h : OrderBot α
⊢ BddBelow s

case inr
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderClosedTopology α
f g : β → α
inst✝¹ : Nonempty α
inst✝ : TopologicalSpace β
s : Set α
hs : IsCompact s
h : NoBotOrder α
⊢ BddBelow s
exact OrderBot.bddBelow s
case inr
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderClosedTopology α
f g : β → α
inst✝¹ : Nonempty α
inst✝ : TopologicalSpace β
s : Set α
hs : IsCompact s
h : NoBotOrder α
this : s ⊆ ⋃ (a : α), Ioi a
⊢ BddBelow s
case inr
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderClosedTopology α
f g : β → α
inst✝¹ : Nonempty α
inst✝ : TopologicalSpace β
s : Set α
hs : IsCompact s
h : NoBotOrder α
⊢ BddBelow s
have : s ⊆ ⋃ a : α, Ioi a := (@iUnion_Ioi α _ (NoBotOrder.to_noMinOrder α)).symm ▸ subset_univ s
case inr.intro
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderClosedTopology α
f g : β → α
inst✝¹ : Nonempty α
inst✝ : TopologicalSpace β
s : Set α
hs : IsCompact s
h : NoBotOrder α
this : s ⊆ ⋃ (a : α), Ioi a
t : Finset α
ht : s ⊆ ⋃ (i : α) (_ : i ∈ t), Ioi i
⊢ BddBelow s
case inr
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderClosedTopology α
f g : β → α
inst✝¹ : Nonempty α
inst✝ : TopologicalSpace β
s : Set α
hs : IsCompact s
h : NoBotOrder α
this : s ⊆ ⋃ (a : α), Ioi a
⊢ BddBelow s
rcases hs.elim_finite_subcover _ (fun _ => isOpen_Ioi) this with ⟨t, ht⟩
case inr.intro
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderClosedTopology α
f g : β → α
inst✝¹ : Nonempty α
inst✝ : TopologicalSpace β
s : Set α
hs : IsCompact s
h : NoBotOrder α
this : s ⊆ ⋃ (a : α), Ioi a
t : Finset α
ht : s ⊆ ⋃ (i : α) (_ : i ∈ t), Ioi i
C : α
hC : C ∈ lowerBounds ↑t
y : α
hy : y ∈ s
⊢ C ≤ y
case inr.intro
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderClosedTopology α
f g : β → α
inst✝¹ : Nonempty α
inst✝ : TopologicalSpace β
s : Set α
hs : IsCompact s
h : NoBotOrder α
this : s ⊆ ⋃ (a : α), Ioi a
t : Finset α
ht : s ⊆ ⋃ (i : α) (_ : i ∈ t), Ioi i
⊢ BddBelow s
refine t.bddBelow.imp fun C hC y hy => ?_
case inr.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderClosedTopology α
f g : β → α
inst✝¹ : Nonempty α
inst✝ : TopologicalSpace β
s : Set α
hs : IsCompact s
h : NoBotOrder α
this : s ⊆ ⋃ (a : α), Ioi a
t : Finset α
ht : s ⊆ ⋃ (i : α) (_ : i ∈ t), Ioi i
C : α
hC : C ∈ lowerBounds ↑t
y : α
hy : y ∈ s
a : α
ha : a ∈ t
hay : y ∈ Ioi a
⊢ C ≤ y
case inr.intro
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderClosedTopology α
f g : β → α
inst✝¹ : Nonempty α
inst✝ : TopologicalSpace β
s : Set α
hs : IsCompact s
h : NoBotOrder α
this : s ⊆ ⋃ (a : α), Ioi a
t : Finset α
ht : s ⊆ ⋃ (i : α) (_ : i ∈ t), Ioi i
C : α
hC : C ∈ lowerBounds ↑t
y : α
hy : y ∈ s
⊢ C ≤ y
rcases mem_iUnion₂.1 (ht hy) with ⟨a, ha, hay⟩
no goals
case inr.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderClosedTopology α
f g : β → α
inst✝¹ : Nonempty α
inst✝ : TopologicalSpace β
s : Set α
hs : IsCompact s
h : NoBotOrder α
this : s ⊆ ⋃ (a : α), Ioi a
t : Finset α
ht : s ⊆ ⋃ (i : α) (_ : i ∈ t), Ioi i
C : α
hC : C ∈ lowerBounds ↑t
y : α
hy : y ∈ s
a : α
ha : a ∈ t
hay : y ∈ Ioi a
⊢ C ≤ y
exact (hC ha).trans (le_of_lt hay)