English
For any family f_i : α → δ', if BddBelow(range f_i x) for all x and each f_i is upper semicontinuous, then the function x' ↦ ⨅ i f_i x' is upper semicontinuous.
Русский
Пусть для каждой точки x множество диапазонов BddBelow(range f_i x) ограничено снизу и каждый f_i верхнеполупрерывна, тогда x' ↦ ⨅ i f_i x' продолжает быть верхнеполупрерывной.
LaTeX
$$$$\\forall x,\\ BddBelow(\\{f_i(x) : i\\}) \\wedge (\\forall i, \\operatorname{UpperSemicontinuous}(f_i)) \\Rightarrow \\operatorname{UpperSemicontinuous}\\left(\\lambda x', \\inf_i f_i(x')\\right).$$$$
Lean4
theorem upperSemicontinuous_ciInf {f : ι → α → δ'} (bdd : ∀ x, BddBelow (range fun i => f i x))
(h : ∀ i, UpperSemicontinuous (f i)) : UpperSemicontinuous fun x' => ⨅ i, f i x' := fun x =>
upperSemicontinuousAt_ciInf (Eventually.of_forall bdd) fun i => h i x
