compContinuousMap_comp — Mathlib

English

compContinuousMap is compatible with composition: compContinuousMap(ψ₂ ∘ ψ₁) = (compContinuousMap ψ₁) ∘ (compContinuousMap ψ₂).

Русский

compContinuousMap совместим с композицией: compContinuousMap(ψ₂ ∘ ψ₁) = (compContinuousMap ψ₁) ∘ (compContinuousMap ψ₂).

LaTeX

$$$compContinuousMap(\\\\psi_2 \\\\circ \\\\psi_1) = (compContinuousMap \\\\psi_1) \\\\circ (compContinuousMap \\\\psi_2)$$$

Lean4

/-- `WeakDual.CharacterSpace.compContinuousMap` is functorial. -/
@[simp]
theorem compContinuousMap_comp (ψ₂ : B →⋆ₐ[𝕜] C) (ψ₁ : A →⋆ₐ[𝕜] B) :
    compContinuousMap (ψ₂.comp ψ₁) = (compContinuousMap ψ₁).comp (compContinuousMap ψ₂) :=
  ContinuousMap.ext fun _a => ext fun _x => rfl

Похожие утверждения