coe_constVSub

Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

URI: https://scilib.ai/kg/mathlib#AffineEquiv.coe_constVSub

English

The map p ↦ p +ᵥ v is an affine equivalence between P1 and itself with tangent space V1.

Русский

Отображение p ↦ p +ᵥ v является аффинным эквивалентом между P1 и самим собой с касательным пространством V1.

LaTeX

$$$\mathrm{constVAdd}_{v} : P_1 \to^a_k P_1, \quad p \mapsto p +_v v$$$

Lean4

@[simp]
theorem coe_constVSub (p : P₁) : ⇑(constVSub k p) = (p -ᵥ ·) :=
  rfl

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

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

Разделы

Аффилиация

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