α : Type u_3
inst✝⁷ : TopologicalSpace α
β : Type ?u.42638
inst✝⁶ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y z : β
γ : Type u_1
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_2
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
gmon : Monotone g
hf : LowerSemicontinuousWithinAt f univ x
⊢ LowerSemicontinuousWithinAt (g ∘ f) univ x
α : Type u_3
inst✝⁷ : TopologicalSpace α
β : Type ?u.42638
inst✝⁶ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y z : β
γ : Type u_1
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_2
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousAt f x
gmon : Monotone g
⊢ LowerSemicontinuousAt (g ∘ f) x
simp only [← lowerSemicontinuousWithinAt_univ_iff] at hf⊢
no goals
α : Type u_3
inst✝⁷ : TopologicalSpace α
β : Type ?u.42638
inst✝⁶ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y z : β
γ : Type u_1
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_2
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
gmon : Monotone g
hf : LowerSemicontinuousWithinAt f univ x
⊢ LowerSemicontinuousWithinAt (g ∘ f) univ x
exact hg.comp_lowerSemicontinuousWithinAt hf gmon