Theorems · Theorem · functional analysis

PolynormableSpace.banach_steinhaus

∀ {ι : Type u_2} {𝕜₁ : Type u_4} {𝕜₂ : Type u_5} {E : Type u_6} {F : Type u_7} [inst : NontriviallyNormedField 𝕜₁]
  [inst_1 : NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜₁ →+* 𝕜₂} [RingHomIsometric σ₁₂] [inst_3 : AddCommGroup E]
  [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜₁ E] [inst_6 : Module 𝕜₂ F] [inst_7 : UniformSpace E]
  [inst_8 : UniformSpace F] [IsUniformAddGroup E] [IsUniformAddGroup F] [ContinuousSMul 𝕜₁ E] [BarrelledSpace 𝕜₁ E]
  {𝓕 : ι → E →SL[σ₁₂] F} [PolynormableSpace 𝕜₂ F],
  (∀ (x : E), Bornology.IsVonNBounded 𝕜₂ (Set.range fun i => (𝓕 i) x)) → UniformEquicontinuous (DFunLike.coe ∘ 𝓕)

The Banach-Steinhaus theorem, or Uniform Boundedness Principle, for maps from a barrelled space to any polynormable space.

Defined in

Mathlib.Analysis.LocallyConvex.Barrelled

Cited by

0 results in Mathlib

Foundations

Depth 166 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNontriviallyNormedFieldRingHomIsometricAddCommGroupAddCommGroupModuleModuleUniformSpaceUniformSpaceIsUniformAddGroupIsUniformAddGroupContinuousSMulBarrelledSpacePolynormableSpace