upperSemicontinuous_iInf — Mathlib

English

If every f_i is upper semicontinuous, then the pointwise infimum x' ↦ ⨅ i f_i x' is upper semicontinuous.

Русский

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

LaTeX

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

Lean4

theorem upperSemicontinuous_iInf {f : ι → α → δ} (h : ∀ i, UpperSemicontinuous (f i)) :
    UpperSemicontinuous fun x' => ⨅ i, f i x' := fun x => upperSemicontinuousAt_iInf fun i => h i x

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