α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type ?u.183589
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y z : β
ι : Type ?u.183615
γ : Type u_2
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
hf : UpperSemicontinuousWithinAt f univ x
hg : UpperSemicontinuousWithinAt g univ x
⊢ UpperSemicontinuousWithinAt (fun z => f z + g z) univ x
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type ?u.183589
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y z : β
ι : Type ?u.183615
γ : Type u_2
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : UpperSemicontinuousAt f x
hg : UpperSemicontinuousAt g x
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
⊢ UpperSemicontinuousAt (fun z => f z + g z) x
simp_rw [← upperSemicontinuousWithinAt_univ_iff] at *
no goals
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type ?u.183589
inst✝³ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y z : β
ι : Type ?u.183615
γ : Type u_2
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x)
hf : UpperSemicontinuousWithinAt f univ x
hg : UpperSemicontinuousWithinAt g univ x
⊢ UpperSemicontinuousWithinAt (fun z => f z + g z) univ x
exact hf.add' hg hcont