lift_apply_mk — Mathlib

English

For f: M →* P and g: N →* P and x in FreeMonoid(M ⊕ N), lift f g (mk x) = FreeMonoid.lift (Sum.elim f g) x.

Русский

Для отображений f: M →* P и g: N →* P и элемента x ∈ FreeMonoid(M ⊕ N): lift f g (mk x) = FreeMonoid.lift (Sum.elim f g) x.

LaTeX

$$$ \mathrm{lift}(f,g)(\mathrm{mk}(x)) = \mathrm{FreeMonoid.lift}(\mathrm{Sum.elim} f g)(x) $$$

Lean4

@[to_additive (attr := simp)]
theorem lift_apply_mk (f : M →* P) (g : N →* P) (x : FreeMonoid (M ⊕ N)) :
    lift f g (mk x) = FreeMonoid.lift (Sum.elim f g) x :=
  rfl

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