comp_apply — Mathlib

English

The underlying linear map of the composite equals the composition of the underlying maps: (f ≫ g).hom = g.hom ∘ f.hom.

Русский

Векторное отображение композиции равняется композиции соответствующих отображений: (f ≫ g).hom = g.hom ∘ f.hom.

LaTeX

$$$ (f \\gg g).hom = g.hom \\circ f.hom. $$$

Lean4

theorem comp_apply {M N O : ModuleCat.{v} R} (f : M ⟶ N) (g : N ⟶ O) (x : M) : (f ≫ g) x = g (f x) := by simp

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