English
The inside sum (within a set s) of two lower semicontinuous functions is lower semicontinuous.
Русский
Сумма внутри множества лс-функций — лс.
LaTeX
$$$\\text{LowerSemicontinuousWithinAt } f s x \\land \\text{LowerSemicontinuousWithinAt } g s x \\Rightarrow \\text{LowerSemicontinuousWithinAt } (f+ g) s x$$$
Lean4
theorem lowerSemicontinuousWithinAt_sum {f : ι → α → γ} {a : Finset ι}
(ha : ∀ i ∈ a, LowerSemicontinuousWithinAt (f i) s x) : LowerSemicontinuousWithinAt (fun z => ∑ i ∈ a, f i z) s x :=
by
classical
induction a using Finset.induction_on with
| empty => exact lowerSemicontinuousWithinAt_const
| insert _ _ ia IH =>
simp only [ia, Finset.sum_insert, not_false_iff]
exact
LowerSemicontinuousWithinAt.add (ha _ (Finset.mem_insert_self ..))
(IH fun j ja => ha j (Finset.mem_insert_of_mem ja))
