English
Let p(i) be a family of propositions, and f_i hi : α → δ' a family of functions indexed by i and a witness hi. If each f_i hi is upper semicontinuous within s at x, then the n-ary infimum over i and hi of f_i hi(x') is upper semicontinuous within s at x.
Русский
Пусть имеется семейство индексов i и условий hi; если каждая функция f_i hi верхнеполупрерывна внутри s в x, то f(x') = ⨅ (i)(hi), f_i hi(x') верхнеполупрерывна внутри s в x.
LaTeX
$$$$\\operatorname{UpperSemicontinuousWithinAt}\\left(\\lambda x', \\inf_i \\inf_{h_i} f_i(h_i)(x'), s, x\\right).$$$$
Lean4
theorem upperSemicontinuousWithinAt_biInf {p : ι → Prop} {f : ∀ i, p i → α → δ}
(h : ∀ i hi, UpperSemicontinuousWithinAt (f i hi) s x) :
UpperSemicontinuousWithinAt (fun x' => ⨅ (i) (hi), f i hi x') s x :=
upperSemicontinuousWithinAt_iInf fun i => upperSemicontinuousWithinAt_iInf fun hi => h i hi
