lowerSemicontinuousOn_iSup — Mathlib

English

Let f_i: α → δ' with δ' ConditionallyCompleteLinearOrder. If a BddAbove condition holds near x and each f_i is LowerSemicontinuousAt (f_i) x, then x' ↦ ⨆ i f_i x' is LowerSemicontinuousAt at x.

Русский

Пусть f_i: α → δ' и δ' имеет CCCL порядок; при условии верхней границы в окрестности x и если каждый f_i лц в x, тогда iSup(f_i) лc в x.

LaTeX

$$$\\displaystyle \\Big(\\forall i,\\ LowerSemicontinuousAt(f_i,x)\\Big) \\Rightarrow \\ LowerSemicontinuousAt\\Big( x' \\mapsto \\bigsqcup_i f_i(x') , x \\Big)$$$

Lean4

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

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