homothety — Mathlib

English

The homothety about a center c with scale r is the affine map sending p to r(p − c) + c.

Русский

Гомотетия относительно центра c с коэффициентом масштаба r — аффинное отображение, отправляющее точку p в r(p − c) + c.

LaTeX

$$$\operatorname{homothety}(c,r)(p) = r\,(p - c) + c$$$

Lean4

/-- `homothety c r` is the homothety (also known as dilation) about `c` with scale factor `r`. -/
def homothety (c : P1) (r : k) : P1 →ᵃ[k] P1 :=
  r • (id k P1 -ᵥ const k P1 c) +ᵥ const k P1 c

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