comp_apply — Mathlib

English

Let f: β →*o γ and g: α →*o β be order-preserving monoid homomorphisms. Then the composite f ∘ g, when applied to any a ∈ α, satisfies (f ∘ g)(a) = f(g(a)).

Русский

Пусть f: β →*o γ и g: α →*o β — упорядоченные моноид-гомоморфизмы. Тогда композиция f ∘ g, применённая к a ∈ α, удовлетворяет (f ∘ g)(a) = f(g(a)).

LaTeX

$$$ \forall a,\ (f \circ g)(a) = f(g(a)). $$$

Lean4

@[to_additive (attr := simp)]
theorem comp_apply (f : β →*o γ) (g : α →*o β) (a : α) : (f.comp g) a = f (g a) :=
  rfl

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