English
Let f_i : α → δ' be functions, and suppose a family of upper semicontinuous within-at functions is given. Then the infimum over i, x ↦ ⨅ i f_i(x) is upper semicontinuous within at x, provided a suitable bounded-below condition holds along nearby points.
Русский
Пусть f_i : α → δ' и имеется семейство функций верхней полупрерывности внутри множества s в точке x; тогда ∀ x, x ↦ ⨅ i f_i(x) верхнеполупрерывна внутри s при некоторых условиях ограничения снизу рядом с x.
LaTeX
$$$$\\text{bdd} : \\forall i,\\ \\text{UpperSemicontinuousWithinAt}(f_i,s,x) \\Rightarrow \\operatorname{UpperSemicontinuousWithinAt}\\bigl(\\lambda x', \\inf_i f_i(x'), s, x\\bigr).$$$$
Lean4
theorem upperSemicontinuousWithinAt_ciInf {f : ι → α → δ'} (bdd : ∀ᶠ y in 𝓝[s] x, BddBelow (range fun i => f i y))
(h : ∀ i, UpperSemicontinuousWithinAt (f i) s x) : UpperSemicontinuousWithinAt (fun x' => ⨅ i, f i x') s x :=
@lowerSemicontinuousWithinAt_ciSup α _ x s ι δ'ᵒᵈ _ f bdd h
