lowerSemicontinuous_biSup — Mathlib

English

If every f_i is LowerSemicontinuousOn (f_i) s, then x ↦ iSup_i f_i(x) is LowerSemicontinuousOn (f) s.

Русский

Если каждая f_i лс на s, то iSup_i f_i(x) лс на s.

LaTeX

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

Lean4

theorem lowerSemicontinuous_biSup {p : ι → Prop} {f : ∀ i, p i → α → δ} (h : ∀ i hi, LowerSemicontinuous (f i hi)) :
    LowerSemicontinuous fun x' => ⨆ (i) (hi), f i hi x' :=
  lowerSemicontinuous_iSup fun i => lowerSemicontinuous_iSup fun hi => h i hi

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