comp_val — Mathlib

English

The value of a composite morphism f ≫ g in the action category is the product of the values of g and f in M, in that order.

Русский

Значение композиции f ≫ g в категории действия равно произведению значений g и f в M в указанном порядке.

LaTeX

$$$\big((f \gg g).\text{val}\big) = g.\text{val} \cdot f.\text{val}$$$

Lean4

@[simp]
protected theorem comp_val {x y z : ActionCategory M X} (f : x ⟶ y) (g : y ⟶ z) : (f ≫ g).val = g.val * f.val :=
  rfl

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