upperSemicontinuousOn_iInf — Mathlib

English

If all f_i are upper semicontinuousOn s, then the pointwise infimum x' ↦ ⨅ i f_i x' is upper semicontinuousOn s.

Русский

Если все f_i верхнеполупрерывны на s, то f(x') = ⨅ i f_i(x') верхнеполупрерывна на s.

LaTeX

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

Lean4

theorem upperSemicontinuousOn_iInf {f : ι → α → δ} (h : ∀ i, UpperSemicontinuousOn (f i) s) :
    UpperSemicontinuousOn (fun x' => ⨅ i, f i x') s := fun x hx => upperSemicontinuousWithinAt_iInf fun i => h i x hx

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