lowerSemicontinuousWithinAt_iSup — Mathlib

English

If each f_i is LowerSemicontinuousWithinAt (f_i) s x, then the function x' ↦ ⨆ i f_i(x') is lower semicontinuous within s at x.

Русский

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

LaTeX

$$$\\displaystyle \\Big(\\forall i,\\ LowerSemicontinuousWithinAt(f_i,s,x)\\Big) \\Rightarrow \\ LowerSemicontinuousWithinAt\\Big( x' \\mapsto \\bigsqcup_i f_i(x') , s \\Big)\\; x$$$

Lean4

theorem lowerSemicontinuousWithinAt_iSup {f : ι → α → δ} (h : ∀ i, LowerSemicontinuousWithinAt (f i) s x) :
    LowerSemicontinuousWithinAt (fun x' => ⨆ i, f i x') s x :=
  lowerSemicontinuousWithinAt_ciSup (by simp) h

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