pointwise_vadd_direction

Mathlib.LinearAlgebra.AffineSpace.Pointwise

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

← MathLib Explorer

English

The direction (direction subspace) of v +ᵥ s equals the direction of s.

Русский

Направление v +ᵥ s равно направлению s.

LaTeX

$$$\mathrm{direction}(v +\!\!\! s) = \mathrm{direction}(s).$$$

Lean4

theorem pointwise_vadd_direction (v : V) (s : AffineSubspace k P) : (v +ᵥ s).direction = s.direction :=
  by
  rw [pointwise_vadd_eq_map, map_direction]
  exact Submodule.map_id _

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

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

Разделы

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

Аффилиация

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