case inl
α : Type u
β : Type v
γ : Type w
inst✝⁶ : CompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : CompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderClosedTopology β
inst✝ : Nonempty γ
f : α → β
s : Set α
Cf : ContinuousAt f (sSup s)
Mf : Monotone f
fbot : f ⊥ = ⊥
h : s = ∅
⊢ f (sSup s) = sSup (f '' s)

case inr
α : Type u
β : Type v
γ : Type w
inst✝⁶ : CompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : CompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderClosedTopology β
inst✝ : Nonempty γ
f : α → β
s : Set α
Cf : ContinuousAt f (sSup s)
Mf : Monotone f
fbot : f ⊥ = ⊥
h : Set.Nonempty s
⊢ f (sSup s) = sSup (f '' s)
α : Type u
β : Type v
γ : Type w
inst✝⁶ : CompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : CompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderClosedTopology β
inst✝ : Nonempty γ
f : α → β
s : Set α
Cf : ContinuousAt f (sSup s)
Mf : Monotone f
fbot : f ⊥ = ⊥
⊢ f (sSup s) = sSup (f '' s)
cases' s.eq_empty_or_nonempty with h h
no goals
case inl
α : Type u
β : Type v
γ : Type w
inst✝⁶ : CompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : CompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderClosedTopology β
inst✝ : Nonempty γ
f : α → β
s : Set α
Cf : ContinuousAt f (sSup s)
Mf : Monotone f
fbot : f ⊥ = ⊥
h : s = ∅
⊢ f (sSup s) = sSup (f '' s)
simp [h, fbot]
no goals
case inr
α : Type u
β : Type v
γ : Type w
inst✝⁶ : CompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : CompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderClosedTopology β
inst✝ : Nonempty γ
f : α → β
s : Set α
Cf : ContinuousAt f (sSup s)
Mf : Monotone f
fbot : f ⊥ = ⊥
h : Set.Nonempty s
⊢ f (sSup s) = sSup (f '' s)
exact Mf.map_sSup_of_continuousAt' Cf h