instId_comp — Mathlib

English

If φ is a function and ψ is the identity on N, then CompTriple φ ψ φ holds with comp_eq expressing ψ ∘ φ = φ.

Русский

Если ψ — тождество на N, то CompTriple φ ψ φ истинно и comp_eq выражает ψ ∘ φ = φ.

LaTeX

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

Lean4

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

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