pointwise_vadd_bot

Mathlib.LinearAlgebra.AffineSpace.Pointwise

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

English

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

Русский

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

LaTeX

$$$v +\!\!\! (\top : \mathrm{AffineSubspace}\ k\ P) = \top.$$$

Lean4

@[simp]
theorem pointwise_vadd_bot (v : V) : v +ᵥ (⊥ : AffineSubspace k P) = ⊥ := by ext; simp [pointwise_vadd_eq_map, map_bot]

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

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

Разделы

Аффилиация

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