map_pointwise_vadd

Mathlib.LinearAlgebra.AffineSpace.Pointwise

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

← MathLib Explorer

English

Translation by any vector preserves the top element: v +ᵥ ⊤ = ⊤.

Русский

Перенос на вектор сохраняет верх: v +ᵥ ⊤ = ⊤.

LaTeX

$$$v +\!\!\top = \top.$$$

Lean4

theorem map_pointwise_vadd (f : P₁ →ᵃ[k] P₂) (v : V₁) (s : AffineSubspace k P₁) :
    (v +ᵥ s).map f = f.linear v +ᵥ s.map f :=
  by
  rw [pointwise_vadd_eq_map, pointwise_vadd_eq_map, map_map, map_map]
  congr 1
  ext
  exact f.map_vadd _ _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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