clift_apply_mk — Mathlib

English

The lift applied to the free monoid constructor preserves mk, i.e., for any word w, clift f hM1 hN1 hM hN (mk w) = f w.

Русский

Лифтинг сохраняет отображение mk: для любого слова w выполняется clift f ... (mk w) = f w.

LaTeX

$$$ clift(f,h_M1,h_N1,h_M,h_N)(\mathrm{mk}(w)) = f(w).$$$

Lean4

@[to_additive (attr := simp)]
theorem clift_apply_mk (f : FreeMonoid (M ⊕ N) →* P) (hM₁ hN₁ hM hN w) : clift f hM₁ hN₁ hM hN (mk w) = f w :=
  rfl

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