mapRange_sub' — Mathlib

English

A variant of mapRange subtraction: mapRange f hf (v1 - v2) = mapRange f hf v1 - mapRange f hf v2.

Русский

Вариант mapRange для разности: mapRange f hf (v1 - v2) = mapRange f hf v1 - mapRange f hf v2.

LaTeX

$$$\forall v_1,v_2:\ ι \to_{0} G:\ mapRange\ f\ hf\ (v_1 - v_2) = mapRange\ f\ hf\ v_1 - mapRange\ f\ hf\ v_2$$$

Lean4

theorem mapRange_sub' [SubtractionMonoid H] [FunLike F G H] [AddMonoidHomClass F G H] {f : F} (v₁ v₂ : ι →₀ G) :
    mapRange f (map_zero f) (v₁ - v₂) = mapRange f (map_zero f) v₁ - mapRange f (map_zero f) v₂ :=
  mapRange_sub (map_sub f) v₁ v₂

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