upperSemicontinuousWithinAt_iInf — Mathlib

English

If for each i, f_i is upper semicontinuous within s at x, then the function x' ↦ ⨅ i, f_i(x') is upper semicontinuous within s at x.

Русский

Если для каждого i функция f_i верхнеполупрерывна внутри s в x, то x' ↦ ⨅ i f_i(x') верхнеполупрерывна внутри s в x.

LaTeX

$$$$\\forall i,\\ \\operatorname{UpperSemicontinuousWithinAt}(f_i,s,x) \\Rightarrow \\operatorname{UpperSemicontinuousWithinAt}\\left(\\lambda x',\\inf_i f_i(x'), s, x\\right).$$$$

Lean4

theorem upperSemicontinuousWithinAt_iInf {f : ι → α → δ} (h : ∀ i, UpperSemicontinuousWithinAt (f i) s x) :
    UpperSemicontinuousWithinAt (fun x' => ⨅ i, f i x') s x :=
  @lowerSemicontinuousWithinAt_iSup α _ x s ι δᵒᵈ _ f h

Похожие утверждения