Theorems · Theorem · functional analysis

NormedSpace.equicontinuous_TFAE

∀ {𝕜 : Type u_1} {𝕜₂ : Type u_3} {E : Type u_5} {F : Type u_6} {ι : Type u_9} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_2 : RingHomIsometric σ₁₂]
  [inst_3 : SeminormedAddCommGroup E] [inst_4 : SeminormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 E]
  [inst_6 : NormedSpace 𝕜₂ F] (f : ι → E →SL[σ₁₂] F),
  [EquicontinuousAt (DFunLike.coe ∘ f) 0, Equicontinuous (DFunLike.coe ∘ f), UniformEquicontinuous (DFunLike.coe ∘ f),
      ∃ C, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖, ∃ C ≥ 0, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖,
      ∃ C, ∀ (i : ι), ‖f i‖ ≤ C, ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C, BddAbove (Set.range fun x => ‖f x‖),
      ⨆ i, ↑‖f i‖₊ < ⊤].TFAE

Equivalent characterizations for equicontinuity of a family of continuous linear maps between normed spaces. See also WithSeminorms.equicontinuous_TFAE for similar characterizations between spaces satisfying WithSeminorms.

Defined in

Mathlib.Analysis.Normed.Operator.NormedSpace

Cited by

2 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNontriviallyNormedFieldRingHomIsometricSeminormedAddCommGroupSeminormedAddCommGroupNormedSpaceNormedSpace