instVAdd — Mathlib

English

There is a translation action of V on the affine basis: translating the basis by a vector v yields another affine basis with the same underlying structure.

Русский

Существует действие переноса по V на аффинную базу: перенесение базы на вектор v даёт другую аффинную базу с той же структурой.

LaTeX

$$$\\text{(v +ᵥ b) is an affine basis with the same structural data as } b$$$

Lean4

instance instVAdd : VAdd V (AffineBasis ι k P) where
  vadd x
    b :=
    { toFun := x +ᵥ ⇑b, ind' := b.ind'.vadd,
      tot' := by
        rw [Pi.vadd_def, ← vadd_set_range, ← AffineSubspace.pointwise_vadd_span, b.tot,
          AffineSubspace.pointwise_vadd_top] }

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