banach_steinhaus_iSup_nnnorm — Mathlib

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)

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