English
If a family of continuous linear maps from a Banach space E to F is pointwise bounded, then the operator norms are uniformly bounded.
Русский
Если семейство непрерывных линейных отображений из Банаха E в нормированное пространство F задано точечно ограниченным, то нормы операторов имеют общую верхнюю границу.
LaTeX
$$Если ∀ x ∈ E, ∃ C с ∀ i, ‖g_i x‖ ≤ C, то ∃ C' с ∀ i, ‖g_i‖ ≤ C'.$$
Lean4
/-- This is the standard Banach-Steinhaus theorem, or Uniform Boundedness Principle.
If a family of continuous linear maps from a Banach space into a normed space is pointwise
bounded, then the norms of these linear maps are uniformly bounded.
See also `WithSeminorms.banach_steinhaus` for the general statement in barrelled spaces. -/
theorem banach_steinhaus {ι : Type*} [CompleteSpace E] {g : ι → E →SL[σ₁₂] F} (h : ∀ x, ∃ C, ∀ i, ‖g i x‖ ≤ C) :
∃ C', ∀ i, ‖g i‖ ≤ C' :=
by
rw [show (∃ C, ∀ i, ‖g i‖ ≤ C) ↔ _ from (NormedSpace.equicontinuous_TFAE g).out 5 2]
refine (norm_withSeminorms 𝕜₂ F).banach_steinhaus (fun _ x ↦ ?_)
simpa [bddAbove_def, forall_mem_range] using h x
