English
If for all x, sup_i ‖g_i x‖ is finite, then sup_i ‖g_i‖ is finite.
Русский
Если для каждого x sup_i ‖g_i x‖ конечно, то sup_i ‖g_i‖ конечен.
LaTeX
$$$\forall x, (\sup_i ||g_i x||_+) < \infty \Rightarrow (\sup_i ||g_i||_+) < \infty$$$
Lean4
/-- This version of Banach-Steinhaus is stated in terms of suprema of `↑‖·‖₊ : ℝ≥0∞`
for convenience. -/
theorem banach_steinhaus_iSup_nnnorm {ι : Type*} [CompleteSpace E] {g : ι → E →SL[σ₁₂] F}
(h : ∀ x, (⨆ i, ↑‖g i x‖₊) < ∞) : (⨆ i, ↑‖g i‖₊) < ∞ :=
by
rw [show ((⨆ i, ↑‖g i‖₊) < ∞) ↔ _ from (NormedSpace.equicontinuous_TFAE g).out 8 2]
refine (norm_withSeminorms 𝕜₂ F).banach_steinhaus (fun _ x ↦ ?_)
simpa [← NNReal.bddAbove_coe, ← Set.range_comp] using ENNReal.iSup_coe_lt_top.1 (h x)