Theorems · Theorem · functional analysis

WithSeminorms.banach_steinhaus

∀ {ι : Type u_2} {κ : Type u_3} {𝕜₁ : 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} {q : SeminormFamily 𝕜₂ F κ},
  WithSeminorms q →
    (∀ (k : κ) (x : E), BddAbove (Set.range fun i => (q k) ((𝓕 i) x))) → UniformEquicontinuous (DFunLike.coe ∘ 𝓕)

The Banach-Steinhaus theorem, or Uniform Boundedness Principle, for maps from a barrelled space to any space whose topology is generated by a family of seminorms. Use WithSeminorms.equicontinuous_TFAE and Seminorm.bound_of_continuous to get explicit bounds on the seminorms from equicontinuity.

Defined in

Mathlib.Analysis.LocallyConvex.Barrelled

Cited by

3 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNontriviallyNormedFieldRingHomIsometricAddCommGroupAddCommGroupModuleModuleUniformSpaceUniformSpaceIsUniformAddGroupIsUniformAddGroupContinuousSMulBarrelledSpace