English
If every i hi satisfies UpperSemicontinuousOn (f i hi) on s, then the infimum over i and hi, f i hi x' is upper semicontinuousOn s at x.
Русский
Если для каждой пары i, hi выполнено UpperSemicontinuousOn (f i hi) на s, то ⨅ (i)(hi) f i hi x' верхнеполупрерывна на s в x.
LaTeX
$$$$\\forall i hi,\\ \\operatorname{UpperSemicontinuousOn}\\left(f_i\\, hi, s\\right) \\Rightarrow \\operatorname{UpperSemicontinuousOn}\\left(\\lambda x', \\inf_i \\inf_{hi} f_i hi(x'), s\\right).$$$$
Lean4
theorem upperSemicontinuousOn_biInf {p : ι → Prop} {f : ∀ i, p i → α → δ}
(h : ∀ i hi, UpperSemicontinuousOn (f i hi) s) : UpperSemicontinuousOn (fun x' => ⨅ (i) (hi), f i hi x') s :=
upperSemicontinuousOn_iInf fun i => upperSemicontinuousOn_iInf fun hi => h i hi
