English
If for each i, f_i is upper semicontinuousWithinAt (s) at x, then the infimum over i, x' ↦ ⨅ i f_i x' is upper semicontinuousWithinAt at x.
Русский
Пусть для каждого i f_i является верхнеполупрерывной внутри s в x; тогда ⨅ i f_i(x') верхнеполупрерывна внутри s в x.
LaTeX
$$$$\\forall i,\\ \\operatorname{UpperSemicontinuousWithinAt}(f_i, s, x) \\Rightarrow \\operatorname{UpperSemicontinuousWithinAt}\\left(\\lambda x', \\inf_i f_i(x'), s, x\\right).$$$$
Lean4
theorem upperSemicontinuousAt_biInf {p : ι → Prop} {f : ∀ i, p i → α → δ}
(h : ∀ i hi, UpperSemicontinuousAt (f i hi) x) : UpperSemicontinuousAt (fun x' => ⨅ (i) (hi), f i hi x') x :=
upperSemicontinuousAt_iInf fun i => upperSemicontinuousAt_iInf fun hi => h i hi
