constVAdd — Mathlib

English

The map p' ↦ p -ᵥ p' is a bijection P → G with inverse p ∈ G ↦ p +ᵥ p'.

Русский

Отображение p' ↦ p -ᵥ p' является биекцией P → G с обратной (взаимной) биекцией p ∈ G ↦ p +ᵥ p'.

LaTeX

$$$\text{ConstVSub}(p): P \to G,\quad p'\mapsto p -ᵥ p'$$$

Lean4

/-- The permutation given by `p ↦ v +ᵥ p`. -/
def constVAdd (v : G) : Equiv.Perm P where
  toFun := (v +ᵥ ·)
  invFun := (-v +ᵥ ·)
  left_inv p := by simp [vadd_vadd]
  right_inv p := by simp [vadd_vadd]

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