English
Let f_i: α → δ' with δ' a ConditionallyCompleteLinearOrder. If a bounded above condition holds near x and each f_i is lower semicontinuous at x, then the function x' ↦ ⨆ i f_i(x') is lower semicontinuous at x.
Русский
Пусть f_i: α → δ' над частично упорядкованным линейным порядком δ'. При условии верхней ограниченности поблизости x и если каждый f_i ниже полупрерывна в x, то x' ↦ ⨆ i f_i(x') л.с. в x.
LaTeX
$$$\\displaystyle \\Big(\\forall i,\\ LowerSemicontinuousAt(f_i,x)\\Big) \\Rightarrow \\ LowerSemicontinuousAt\\Big( x' \\mapsto \\bigsqcup_i f_i(x') , x \\Big)$$$
Lean4
theorem lowerSemicontinuousAt_ciSup {f : ι → α → δ'} (bdd : ∀ᶠ y in 𝓝 x, BddAbove (range fun i => f i y))
(h : ∀ i, LowerSemicontinuousAt (f i) x) : LowerSemicontinuousAt (fun x' => ⨆ i, f i x') x :=
by
simp_rw [← lowerSemicontinuousWithinAt_univ_iff] at *
rw [← nhdsWithin_univ] at bdd
exact lowerSemicontinuousWithinAt_ciSup bdd h
