affineSegment_image — Mathlib

English

Affine maps take affine segments to affine segments: the image of the segment between x and y is the segment between f(x) and f(y).

Русский

Аффинные отображения переводят афинные отрезки: образ отрезка между x и y — это отрезок между f(x) и f(y).

LaTeX

$$$f''\operatorname{affineSegment}(R,x,y) = \operatorname{affineSegment}(R,f(x),f(y)).$$$

Lean4

@[simp]
theorem affineSegment_image (f : P →ᵃ[R] P') (x y : P) : f '' affineSegment R x y = affineSegment R (f x) (f y) :=
  by
  rw [affineSegment, affineSegment, Set.image_image, ← comp_lineMap]
  rfl

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