clift_apply_inl — Mathlib

English

The lift applied to the left injection equals the image under f of the corresponding left-injected generator.

Русский

Лифтинг на левом внедрении равен образу под f соответствующего левого генератора.

LaTeX

$$$ clift(f,h_M1,h_N1,h_M,h_N)(inl x) = f(of(\mathrm{Sum.inl} x)).$$$

Lean4

@[to_additive (attr := simp)]
theorem clift_apply_inl (f : FreeMonoid (M ⊕ N) →* P) (hM₁ hN₁ hM hN) (x : M) :
    clift f hM₁ hN₁ hM hN (inl x) = f (of (.inl x)) :=
  rfl

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