comp_apply — Mathlib

English

Given copies g : Copy B C and f : Copy A B, the application of the composed copy to an element a ∈ A coincides with first applying f to a and then applying g to the result: g.comp f a = g (f a).

Русский

Пусть есть копии g : Copy B C и f : Copy A B; применение композиции копий к элементу a ∈ A совпадает с последовательным применением сначала f к a, затем g к результату: g.comp f a = g (f a).

LaTeX

$$$ g.comp f a = g (f a) $$$

Lean4

@[simp]
theorem comp_apply (g : Copy B C) (f : Copy A B) (a : α) : g.comp f a = g (f a) :=
  RelHom.comp_apply g.toHom f.toHom a

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