pointwise_vadd_span

Mathlib.LinearAlgebra.AffineSpace.Pointwise

URI: https://scilib.ai/kg/mathlib#AffineSubspace.pointwise_vadd_span

English

The translate of an affine span by v equals the affine span of the translate by v.

Русский

Перенос на v образует эквивалентно переносимый выпуклый охватывающий слой.

LaTeX

$$$v +\!\!\! \mathrm{affineSpan}(k, s) = \mathrm{affineSpan}(k, v +\!\!\! s).$$$

Lean4

theorem pointwise_vadd_span (v : V) (s : Set P) : v +ᵥ affineSpan k s = affineSpan k (v +ᵥ s) :=
  map_span _ s

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru