English
Let f_i : α → δ' be a family and suppose ∀ᶠ y in 𝓝 x, BddBelow (range f_i(y)). If each f_i is upper semicontinuous at x, then the infimum over i, i.e., ⨅ i, f_i x', is upper semicontinuous at x.
Русский
Пусть f_i : α → δ' и при этом существует окрестность 𝓝 x такая, что диапазоны range f_i(y) ограничены снизу; если каждый f_i верхнеполупрерывен в x, то ⨅ i f_i(x') верхнеполупрерывна в x.
LaTeX
$$$$\\text{bdd} : \\forall^{} i,\\; \\operatorname{UpperSemicontinuousAt}(f_i,x) \\Rightarrow \\operatorname{UpperSemicontinuousAt}\\left(\\lambda x', \\inf_i f_i(x')\\right) x.$$$$
Lean4
theorem upperSemicontinuousAt_ciInf {f : ι → α → δ'} (bdd : ∀ᶠ y in 𝓝 x, BddBelow (range fun i => f i y))
(h : ∀ i, UpperSemicontinuousAt (f i) x) : UpperSemicontinuousAt (fun x' => ⨅ i, f i x') x :=
@lowerSemicontinuousAt_ciSup α _ x ι δ'ᵒᵈ _ f bdd h
