English
If for all i hi we have LowerSemicontinuousWithinAt (f i hi) s, then x' ↦ ⨆ (i) (hi) f i hi x' is lower semicontinuous within s.
Русский
Если для всех i и hi выполняется LowerSemicontinuousWithinAt(f_i, hi) внутри s, то x' ↦ ⨆ (i) (hi) f_i hi(x') лс внутри s.
LaTeX
$$$\\displaystyle \\Big(\\forall i\\; \\forall hi,\\ LowerSemicontinuousWithinAt(f_i,hi,s,x)\\Big) \\Rightarrow \\ LowerSemicontinuousWithinAt\\Big( x' \\mapsto \\bigsqcup_i f_i hi(x') , s \\Big)\\; x$$$
Lean4
theorem lowerSemicontinuousAt_biSup {p : ι → Prop} {f : ∀ i, p i → α → δ}
(h : ∀ i hi, LowerSemicontinuousAt (f i hi) x) : LowerSemicontinuousAt (fun x' => ⨆ (i) (hi), f i hi x') x :=
lowerSemicontinuousAt_iSup fun i => lowerSemicontinuousAt_iSup fun hi => h i hi
