mapRange_sub — Mathlib

English

For v1,v2 in ι →₀ G, mapRange respects subtraction: mapRange f hf (v1 - v2) = mapRange f hf v1 - mapRange f hf v2.

Русский

Для v1,v2 ∈ ι →₀ G отображение mapRange по сохранению hf учитывает вычитание: 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 [SubNegZeroMonoid G] [SubNegZeroMonoid H] {f : G → H} {hf : f 0 = 0}
    (hf' : ∀ x y, f (x - y) = f x - f y) (v₁ v₂ : ι →₀ G) :
    mapRange f hf (v₁ - v₂) = mapRange f hf v₁ - mapRange f hf v₂ :=
  ext fun _ => by simp only [hf', sub_apply, mapRange_apply]

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