α : Type u
β : Type v
γ : Type w
inst✝⁶ : CompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : CompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderClosedTopology β
inst✝ : Nonempty γ
ι : Sort u_1
f : α → β
g : ι → α
Cf : ContinuousAt f (iSup g)
Mf : Monotone f
fbot : f ⊥ = ⊥
⊢ sSup (range (f ∘ g)) = sSup (range fun i => f (g i))
α : Type u
β : Type v
γ : Type w
inst✝⁶ : CompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : CompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderClosedTopology β
inst✝ : Nonempty γ
ι : Sort u_1
f : α → β
g : ι → α
Cf : ContinuousAt f (iSup g)
Mf : Monotone f
fbot : f ⊥ = ⊥
⊢ f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)
rw [iSup, Mf.map_sSup_of_continuousAt Cf fbot, ← range_comp, iSup]
no goals
α : Type u
β : Type v
γ : Type w
inst✝⁶ : CompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : CompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderClosedTopology β
inst✝ : Nonempty γ
ι : Sort u_1
f : α → β
g : ι → α
Cf : ContinuousAt f (iSup g)
Mf : Monotone f
fbot : f ⊥ = ⊥
⊢ sSup (range (f ∘ g)) = sSup (range fun i => f (g i))
rfl