mul_seq — Mathlib

English

For f,g in FreeSemigroup (α → β) and x in FreeSemigroup α, we have (f · g) <*> x = (f <*> x) · (g <*> x).

Русский

Для f,g ∈ FreeSemigroup (α → β) и x ∈ FreeSemigroup α выполняется (f · g) <*> x = (f <*> x) · (g <*> x).

LaTeX

$$$(f * g) <*> x = (f <*> x) * (g <*> x)$$$

Lean4

@[to_additive (attr := simp)]
theorem mul_seq {f g : FreeSemigroup (α → β)} {x : FreeSemigroup α} : f * g <*> x = (f <*> x) * (g <*> x) :=
  mul_bind _ _ _

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