symm_eq — Mathlib

English

If φ is bijective, then the symmetry operation on the associated affine equivalence agrees with the symmetry of the underlying bijection.

Русский

Если φ биективно, то симметрический переход к сопряжённой аффинной эквивалентности совпадает с симметрией базовой биекция.

LaTeX

$$$(\text{ofBijective }h_\phi).{\text{symm}} = (\text{Equiv.ofBijective } _ h_\phi).{\text{symm}}$$$

Lean4

theorem symm_eq {φ : P₁ →ᵃ[k] P₂} (hφ : Function.Bijective φ) :
    (ofBijective hφ).symm.toEquiv = (Equiv.ofBijective _ hφ).symm :=
  rfl

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