constVSub — Mathlib

English

For a fixed p ∈ P, the map p' ↦ p -ᵥ p' is a bijection P → G with inverse p ∈ G ↦ p +ᵥ p.

Русский

Для фиксированного p ∈ P отображение p' ↦ p -ᵥ p' задаёт биекцию P → G, обратная — p ∈ G ↦ p +ᵥ p.

LaTeX

$$$\text{ConstVSub}(p): P \to G,\quad \text{toFun}(p')(= p -ᵥ p')\text{ bijection with inverse } p'' \mapsto p'' +ᵥ p$$$

Lean4

/-- `p' ↦ p -ᵥ p'` as an equivalence. -/
def constVSub (p : P) : P ≃ G where
  toFun := (p -ᵥ ·)
  invFun := (-· +ᵥ p)
  left_inv p' := by simp
  right_inv v := by simp [vsub_vadd_eq_vsub_sub]

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