induceHom_comp — Mathlib

English

Composition of induced homomorphisms corresponds to the induced homomorphism of the composed maps: (induceHom ψ ψtr) ∘ (induceHom φ φst) = induceHom (ψ ∘ φ) (ψtr ∘ φst).

Русский

Сложение индуцированных гомоморфизмов соответствует индуцированному гомоморфизму от композиции отображений: (induceHom ψ ψtr) ∘ (induceHom φ φst) = induceHom (ψ ∘ φ) (ψtr ∘ φst).

LaTeX

$$$ (induceHom ψ ψtr) \circ (induceHom φ φst) = induceHom(ψ \circ φ)(ψtr \circ φst) $$$

Lean4

@[simp]
theorem induceHom_comp : (induceHom ψ ψtr).comp (induceHom φ φst) = induceHom (ψ.comp φ) (ψtr.comp φst) :=
  by
  ext x
  rfl

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