lowerSemicontinuous_iSup — Mathlib

English

Let s ⊆ α be a set. If for all x ∈ s the range {f_i(x)} is bounded above and each f_i is LowerSemicontinuousOn (f_i) s, then x ↦ ⨆ i f_i(x) is LowerSemicontinuousOn (f) s.

Русский

Пусть s ⊆ α. Если для всех x ∈ s диапазон {f_i(x)} ограничен сверху и каждая f_i lsc на s, то x ↦ ⨆ i f_i(x) lsc на s.

LaTeX

$$$\\displaystyle \\Big(\\forall x\\in s,\\ BddAbove(\\{f_i(x): i\\in ι\\})\\Big) \\Rightarrow \\ LowerSemicontinuousOn( x \\mapsto \\bigsqcup_i f_i(x) , s)$$$

Lean4

theorem lowerSemicontinuous_iSup {f : ι → α → δ} (h : ∀ i, LowerSemicontinuous (f i)) :
    LowerSemicontinuous fun x' => ⨆ i, f i x' :=
  lowerSemicontinuous_ciSup (by simp) h

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