English
If a family of seminorms p i is each continuous, then their supremum is continuous, provided the family is bounded above.
Русский
Если семейство полуанорм p i содержит каждый непрерывный член, то их суперсума непрерывна при условии ограниченности сверху.
LaTeX
$$Continuous (⨆ i, p i) ́, при условий: ∀ i, Continuous (p i) и BddAbove (range p)$$
Lean4
theorem continuous_iSup {ι : Sort*} {𝕜 E : Type*} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E]
[BarrelledSpace 𝕜 E] (p : ι → Seminorm 𝕜 E) (hp : ∀ i, Continuous (p i)) (bdd : BddAbove (range p)) :
Continuous (⨆ i, p i) := by
rw [← Seminorm.coe_iSup_eq bdd]
refine Seminorm.continuous_of_lowerSemicontinuous _ ?_
rw [Seminorm.coe_iSup_eq bdd]
rw [Seminorm.bddAbove_range_iff] at bdd
convert lowerSemicontinuous_ciSup (f := fun i x ↦ p i x) bdd (fun i ↦ (hp i).lowerSemicontinuous)
exact iSup_apply
