Theorems · Theorem · functional analysis

Seminorm.comp_comp

∀ {𝕜 : Type u_3} {𝕜₂ : Type u_4} {𝕜₃ : Type u_5} {E : Type u_7} {E₂ : Type u_8} {E₃ : Type u_9}
  [inst : SeminormedRing 𝕜] [inst_1 : SeminormedRing 𝕜₂] [inst_2 : SeminormedRing 𝕜₃] {σ₁₂ : 𝕜 →+* 𝕜₂}
  [inst_3 : RingHomIsometric σ₁₂] {σ₂₃ : 𝕜₂ →+* 𝕜₃} [inst_4 : RingHomIsometric σ₂₃] {σ₁₃ : 𝕜 →+* 𝕜₃}
  [inst_5 : RingHomIsometric σ₁₃] [inst_6 : AddCommGroup E] [inst_7 : AddCommGroup E₂] [inst_8 : AddCommGroup E₃]
  [inst_9 : Module 𝕜 E] [inst_10 : Module 𝕜₂ E₂] [inst_11 : Module 𝕜₃ E₃] [inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
  (p : Seminorm 𝕜₃ E₃) (g : E₂ →ₛₗ[σ₂₃] E₃) (f : E →ₛₗ[σ₁₂] E₂), p.comp (g ∘ₛₗ f) = (p.comp g).comp f

Defined in

Mathlib.Analysis.Seminorm

Cited by

0 results in Mathlib

Foundations

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

Assumes

SeminormedRingSeminormedRingSeminormedRingRingHomIsometricRingHomIsometricRingHomIsometricAddCommGroupAddCommGroupAddCommGroupModuleModuleModuleRingHomCompTriple