lift_add_apply — Mathlib

English

The lift respects addition: lift (f+g) = lift f + lift g.

Русский

Поднятие (lift) сохраняет сложение функций: lift (f+g) = lift f + lift g.

LaTeX

$$$\\mathrm{lift}\\ (f+g) = \\mathrm{lift}\,f + \\mathrm{lift}\,g$$$

Lean4

theorem lift_add_apply [AddCommGroup G] (f g : α → G) (a : FreeAbelianGroup α) : lift (f + g) a = lift f a + lift g a :=
  by
  refine FreeAbelianGroup.induction_on a ?_ ?_ ?_ ?_
  · simp only [(lift _).map_zero, zero_add]
  · intro x
    simp only [lift_apply_of, Pi.add_apply]
  · intro x _
    simp only [map_neg, lift_apply_of, Pi.add_apply, neg_add]
  · intro x y hx hy
    simp only [(lift _).map_add, hx, hy, add_add_add_comm]

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