pointwise_vadd_top

Mathlib.LinearAlgebra.AffineSpace.Pointwise

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

English

Simplified version: the previous equality holds for all v.

Русский

Упрощённое утверждение: предыдущее равенство верно для любого v.

LaTeX

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

Lean4

@[simp]
theorem pointwise_vadd_top (v : V) : v +ᵥ (⊤ : AffineSubspace k P) = ⊤ := by ext;
  simp [pointwise_vadd_eq_map, vadd_eq_iff_eq_neg_vadd]

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

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

Разделы

Аффилиация

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