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