map_add — Mathlib

English

Mapping distributes over addition: for any f between additive structures, map f on a + b equals map f on a plus map f on b.

Русский

Переображение через отображение публикует сложение: map f(a + b) = map f a + map f b.

LaTeX

$$$\\\\forall {F} [Add β] [FunLike F α β] [AddHomClass F α β] (f : F) (a b : WithTop α), (a + b).map f = a.map f + b.map f$$$

Lean4

@[simp]
protected theorem map_add {F} [Add β] [FunLike F α β] [AddHomClass F α β] (f : F) (a b : WithTop α) :
    (a + b).map f = a.map f + b.map f := by
  induction a
  · exact (top_add _).symm
  · induction b
    · exact (add_top _).symm
    · rw [map_coe, map_coe, ← coe_add, ← coe_add, ← map_add]
      rfl

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