comp_apply — Mathlib

English

If h is a composition triple φ ψ χ, then ψ(φ x) = χ x for all x.

Русский

Если h — тройка композиции φ ψ χ, то для всех x выполняется ψ(φ x) = χ x.

LaTeX

$$$ \forall {M} {N} {P} {\phi : M \to N} {\psi : N \to P} {\chi : M \to P} (h : CompTriple \phi \psi \chi) (x : M), \; \psi (\phi x) = \chi x$$$

Lean4

theorem comp_apply {M N P : Type*} {φ : M → N} {ψ : N → P} {χ : M → P} (h : CompTriple φ ψ χ) (x : M) : ψ (φ x) = χ x :=
  by rw [← h.comp_eq, Function.comp_apply]

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