comp_apply — Mathlib

English

The result of applying the composition to an argument is the same as applying the outer hom to the result of applying the inner one.

Русский

Результат применения композиции к аргументу равен применению внешнего гомоморфизма к результату применения внутреннего.

LaTeX

$$$\\forall a:\\alpha:\\ (f.comp g)(a) = f(g(a))$$$

Lean4

@[simp]
theorem comp_apply (f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) (a : α) : (f.comp g) a = f (g a) :=
  rfl

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