instComp_id — Mathlib

English

If φ is an identity on N and ψ : N → N with IsId ψ, then composing φ with ψ yields ψ and the triple (φ, ψ, ψ) satisfies the composition equality.

Русский

Если φ — тождество на N и ψ : N → N с IsId ψ, то композиция φ и ψ даёт ψ и triple (φ, ψ, ψ) удовлетворяет равенству композиции.

LaTeX

$$$ \forall {N P} {\phi : N \to N} {\psi : N \to P} [\operatorname{IsId} \phi] : \operatorname{CompTriple} \phi \psi \psi$$$

Lean4

instance instComp_id {N P : Type*} {φ : N → N} [IsId φ] {ψ : N → P} : CompTriple φ ψ ψ where
  comp_eq := by simp only [IsId.eq_id, Function.comp_id]

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