clift_apply_inr — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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