smul_span — Mathlib

English

Scaling a set and then taking its affine span is the same as taking the affine span and then scaling: a • affineSpan k s = affineSpan k (a • s).

Русский

Умножение множества и затем афинное охватывание эквивалентно афинному охватыванию после умножения: a • affineSpan k s = affineSpan k (a • s).

LaTeX

$$$ a \\cdot affineSpan k s = affineSpan k (a \\cdot s) $$$

Lean4

theorem smul_span (a : M) (s : Set V) : a • affineSpan k s = affineSpan k (a • s) :=
  map_span _ s

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