English
If h(i, hi) provides LowerSemicontinuousWithinAt for each i and hi, then the bi-index supremum x ↦ ⨆ (i) (hi), f_i hi x is lower semicontinuous within s at x.
Русский
Если для каждого i и условия hi функция f_i hi имеет нижнюю полупрерывность внутри s в x, то bi-индексная supremum функция тоже l.s.c. внутри s в x.
LaTeX
$$$\\displaystyle \\Big(\\forall i\\, \\forall hi,\\ LowerSemicontinuousWithinAt(f_i,hi,s,x)\\Big) \\Rightarrow \\ LowerSemicontinuousWithinAt\\Big( x' \\mapsto \\bigsqcup_{i}(\\,\\text{hi}\\,) f_i hi(x') , s \\Big)\\; x$$$
Lean4
theorem lowerSemicontinuousWithinAt_biSup {p : ι → Prop} {f : ∀ i, p i → α → δ}
(h : ∀ i hi, LowerSemicontinuousWithinAt (f i hi) s x) :
LowerSemicontinuousWithinAt (fun x' => ⨆ (i) (hi), f i hi x') s x :=
lowerSemicontinuousWithinAt_iSup fun i => lowerSemicontinuousWithinAt_iSup fun hi => h i hi
