English
Let f_i: α → δ' (δ' CCCL). If for all x the range of f_i(x) is bounded above and each f_i is lower semicontinuous, then x ↦ ⨆ i f_i(x) is lower semicontinuous.
Русский
Пусть f_i: α → δ' с CCCL. Если для всех x множество значений f_i(x) ограничено сверху и каждая f_i лс, тогда x ↦ ⨆ i f_i(x) лс.
LaTeX
$$$\\displaystyle \\Big(\\forall x,\\ BddAbove(\\{f_i(x): i\\in\\iota\\})\\Big) \\Rightarrow \\ LowerSemicontinuousAt\\Big( x \\mapsto \\bigsqcup_i f_i(x) , x \\Big)$$$
Lean4
theorem lowerSemicontinuous_ciSup {f : ι → α → δ'} (bdd : ∀ x, BddAbove (range fun i => f i x))
(h : ∀ i, LowerSemicontinuous (f i)) : LowerSemicontinuous fun x' => ⨆ i, f i x' := fun x =>
lowerSemicontinuousAt_ciSup (Eventually.of_forall bdd) fun i => h i x
