coe_toEquiv — Mathlib

English

For an affine equivalence e, the underlying Equiv obtained from its toEquiv component acts as the same function as e itself: the underlying function of e.toEquiv equals e.

Русский

Для аффинного эквивалентного отображения e базовая эквивалентность, полученная через toEquiv, действует так же как сама функция e: e.toEquiv является той же функцией, что и e.

LaTeX

$$$e.toEquiv = e \quad\text{as functions}$$$

Lean4

@[simp]
theorem coe_toEquiv (e : P₁ ≃ᵃ[k] P₂) : ⇑e.toEquiv = e :=
  rfl

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