English
Let f_i: ι → α → δ' with δ' a Conditionally complete linear order, and assume a BddAbove condition along nhdsWithin s of x. If each f_i is LowerSemicontinuousWithinAt (f_i) s x, then the function x' ↦ ⨆ i f_i(x') isLowerSemicontinuousWithinAt at x with respect to s.
Русский
Пусть f_i: ι → α → δ' и δ' — частично упорядоченное линейное множество; при условии ограниченности сверху вдоль nhdsWithin s(x) для x выполняется, что каждый f_i l.s.c. внутри s в x; тогда iSup(f_i) тоже l.s.c. внутри 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_ciSup {f : ι → α → δ'} (bdd : ∀ᶠ y in 𝓝[s] x, BddAbove (range fun i => f i y))
(h : ∀ i, LowerSemicontinuousWithinAt (f i) s x) : LowerSemicontinuousWithinAt (fun x' => ⨆ i, f i x') s x :=
by
cases isEmpty_or_nonempty ι
· simpa only [iSup_of_empty'] using lowerSemicontinuousWithinAt_const
· intro y hy
rcases exists_lt_of_lt_ciSup hy with ⟨i, hi⟩
filter_upwards [h i y hi, bdd] with y hy hy' using hy.trans_le (le_ciSup hy' i)
