English
Let f_i : α → δ' and assume BddBelow(range f_i(x)) for all x ∈ s. If each f_i is upper semicontinuousOn s, then x' ↦ ⨅ i f_i x' is upper semicontinuousOn s.
Русский
Пусть f_i : α → δ' и для всех x ∈ s выполняется ограничение снизу BddBelow (range f_i(x)); если каждый f_i верхнеполупрерывна на s, то x' ↦ ⨅ i f_i x' верхнеполупрерывна на s.
LaTeX
$$$$\\forall x'\\in s,\\ \\operatorname{UpperSemicontinuousOn}\\left(\\lambda x', \\inf_i f_i(x'), s\\right).$$$$
Lean4
theorem upperSemicontinuousOn_ciInf {f : ι → α → δ'} (bdd : ∀ x ∈ s, BddBelow (range fun i => f i x))
(h : ∀ i, UpperSemicontinuousOn (f i) s) : UpperSemicontinuousOn (fun x' => ⨅ i, f i x') s := fun x hx =>
upperSemicontinuousWithinAt_ciInf (eventually_nhdsWithin_of_forall bdd) fun i => h i x hx
