vaddConst — Mathlib

English

For every p ∈ P there is an equivalence v ↦ v +ᵥ p between G and P, with inverse p' ↦ p' -ᵥ p.

Русский

Для каждого p ∈ P существует эквивалентность, отображающая v в v +ᵥ p между G и P, с обратной — p' ↦ p' -ᵥ p.

LaTeX

$$$\exists \phi: G \to P \text{ bijection with } \phi(v)=v +ᵥ p \text{ and } \phi^{-1}(p')=p' -ᵥ p$$$

Lean4

/-- `v ↦ v +ᵥ p` as an equivalence. -/
def vaddConst (p : P) : G ≃ P where
  toFun v := v +ᵥ p
  invFun p' := p' -ᵥ p
  left_inv _ := vadd_vsub _ _
  right_inv _ := vsub_vadd _ _

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