one_apply — Mathlib

English

The identity of morphisms sends the unit element to the unit element: for any G,H in CommGrpCat and g ∈ G, ((1 : G ⟶ H) : G → H) g = 1.

Русский

Тождественный мороморфизм отправляет единицу в единицу: для любых G,H ∈ CommGrpCat и g ∈ G выполняется ((1 : G ⟶ H) : G → H) g = 1.

LaTeX

$$$$ \forall G,H\ (g \in G),\ ((1 : G \rightarrow H) g) = 1. $$$$

Lean4

@[to_additive (attr := simp)]
theorem one_apply (G H : CommGrpCat) (g : G) : ((1 : G ⟶ H) : G → H) g = 1 :=
  rfl

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