English
If f and g are USC functions (not necessarily on a set), their pointwise sum is USC when addition is continuous.
Русский
Если f и g — USC-функции, их пофункциональная сумма — USC, когда сложение непрерывно.
LaTeX
$$$hf : UpperSemicontinuous f,\\ hg : UpperSemicontinuous g\\Rightarrow\\; UpperSemicontinuous (\\lambda x => f(x) + g(x))$$$
Lean4
/-- The sum of two upper semicontinuous functions is upper semicontinuous. Formulated with
`[ContinuousAdd]`. The primed version of the lemma uses an explicit continuity assumption on
addition, for application to `EReal`. -/
theorem add {f g : α → γ} (hf : UpperSemicontinuous f) (hg : UpperSemicontinuous g) :
UpperSemicontinuous fun z => f z + g z :=
hf.add' hg fun _x => continuous_add.continuousAt
