α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderClosedTopology β
inst✝ : Nonempty γ
f : α → β
g : γ → α
Cf : ContinuousAt f (⨆ (i : γ), g i)
Mf : Monotone f
H : BddAbove (range g)
⊢ sSup (range (f ∘ fun i => g i)) = sSup (range fun i => f (g i))
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderClosedTopology β
inst✝ : Nonempty γ
f : α → β
g : γ → α
Cf : ContinuousAt f (⨆ (i : γ), g i)
Mf : Monotone f
H : BddAbove (range g)
⊢ f (⨆ (i : γ), g i) = ⨆ (i : γ), f (g i)
rw [iSup, Mf.map_csSup_of_continuousAt Cf (range_nonempty _) H, ← range_comp, iSup]
no goals
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderClosedTopology β
inst✝ : Nonempty γ
f : α → β
g : γ → α
Cf : ContinuousAt f (⨆ (i : γ), g i)
Mf : Monotone f
H : BddAbove (range g)
⊢ sSup (range (f ∘ fun i => g i)) = sSup (range fun i => f (g i))
rfl