image_vsub_image — Mathlib

English

The vector subtraction image of two affine maps equals the image of a linear map applied to the difference of inputs.

Русский

Образ разности векторов двух аффинных отображений равен образу линейного отображения от разности входов.

LaTeX

$$$f''s -ᵥ f''t = f.linear''(s -ᵥ t)$$$

Lean4

theorem image_vsub_image {s t : Set P1} (f : P1 →ᵃ[k] P2) : f '' s -ᵥ f '' t = f.linear '' (s -ᵥ t) :=
  by
  ext v
  simp only [Set.mem_vsub, Set.mem_image, exists_exists_and_eq_and, ← f.linearMap_vsub]
  grind

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