lowerSemicontinuousOn_biSup — Mathlib

English

Let p: ι → Prop and f_i: ∀ i, p i → α → δ. If for all i hi the function f_i hi is lower semicontinuous on s, then x' ↦ ⨆ (i) (hi) f_i hi x' is lower semicontinuous on s.

Русский

Пусть p(i) задаёт условия, f_i hi: α → δ. Если для всех i и hi f_i hi лс на s, то x' ↦ ⨆ (i) (hi) f_i hi(x') лс на s.

LaTeX

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

Lean4

theorem lowerSemicontinuousOn_biSup {p : ι → Prop} {f : ∀ i, p i → α → δ}
    (h : ∀ i hi, LowerSemicontinuousOn (f i hi) s) : LowerSemicontinuousOn (fun x' => ⨆ (i) (hi), f i hi x') s :=
  lowerSemicontinuousOn_iSup fun i => lowerSemicontinuousOn_iSup fun hi => h i hi

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