English
Let f_i: ι → α → δ' with δ' ConditionallyCompleteLinearOrder. If for all x ∈ s the range {f_i(x)} is bounded above and each f_i is LowerSemicontinuousWithinAt (f_i) s x, then the supremum x' ↦ ⨆ i f_i x' is LowerSemicontinuousWithinAt (f) s x.
Русский
Пусть f_i: ι → α → δ' и δ' — частично упоряд. линейное. При условии верхней ограниченности по x и если каждое f_i lsc внутри s в x, то x' ↦ ⨆ i f_i(x') lsc внутри s в x.
LaTeX
$$$\\displaystyle \\Big(\\forall i,\\ LowerSemicontinuousWithinAt(f_i,s,x)\\Big) \\Rightarrow \\ LowerSemicontinuousWithinAt\\Big( x' \\mapsto \\bigsqcup_i f_i(x') , s \\Big)\\; x$$$
Lean4
theorem lowerSemicontinuousOn_ciSup {f : ι → α → δ'} (bdd : ∀ x ∈ s, BddAbove (range fun i => f i x))
(h : ∀ i, LowerSemicontinuousOn (f i) s) : LowerSemicontinuousOn (fun x' => ⨆ i, f i x') s := fun x hx =>
lowerSemicontinuousWithinAt_ciSup (eventually_nhdsWithin_of_forall bdd) fun i => h i x hx
