toFreeSemigroup_map — Mathlib

English

The natural transformation from FreeMagma to FreeSemigroup commutes with map: toFreeSemigroup (map f x) = FreeSemigroup.map f (toFreeSemigroup x).

Русский

Естественная трансформация от FreeMagma к FreeSemigroup коммутирует с map: toFreeSemigroup (map f x) = FreeSemigroup.map f (toFreeSemigroup x).

LaTeX

$$$\text{toFreeSemigroup} (\text{map } f \, x) = \text{FreeSemigroup.map } f (\text{toFreeSemigroup } x)$$$

Lean4

@[to_additive]
theorem toFreeSemigroup_map (f : α → β) (x : FreeMagma α) :
    toFreeSemigroup (map f x) = FreeSemigroup.map f (toFreeSemigroup x) :=
  DFunLike.congr_fun (toFreeSemigroup_comp_map f) x

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