upperSemicontinuousAt_iInf — Mathlib

English

If f_i : α → β are upper semicontinuous at x for all i, then the infimum f(x) = ⨅ i f_i(x) is upper semicontinuous at x.

Русский

Если для всех i функции f_i верхнеполупрерывны в точке x, то f(x) = ⨅ i f_i(x) верхнеполупрерывна в x.

LaTeX

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

Lean4

theorem upperSemicontinuousAt_iInf {f : ι → α → δ} (h : ∀ i, UpperSemicontinuousAt (f i) x) :
    UpperSemicontinuousAt (fun x' => ⨅ i, f i x') x :=
  @lowerSemicontinuousAt_iSup α _ x ι δᵒᵈ _ f h

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