image_segment — Mathlib

English

For an affine map f, the image of the segment [a -[𝕜] b] is the segment [f(a) -[𝕜] f(b)].

Русский

Для аффинного отображения f образ сегмента [a -[𝕜] b] есть сегмент [f(a) -[𝕜] f(b)].

LaTeX

$$$$ f '' [a -[\mathbb{K}] b] = [f(a) -[\mathbb{K}] f(b)]. $$$$

Lean4

@[simp]
theorem image_segment (f : E →ᵃ[𝕜] F) (a b : E) : f '' [a -[𝕜] b] = [f a -[𝕜] f b] :=
  Set.ext fun x => by simp_rw [segment_eq_image_lineMap, mem_image, exists_exists_and_eq_and, AffineMap.apply_lineMap]

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