symm_toAffineEquiv — Mathlib

English

The inverse of a continuous affine equivalence is defined as a continuous affine equivalence.

Русский

Обратное непрерывному аффинному эквиваленту определяется как непрерывное аффинное эквивалентное отображение.

LaTeX

$$$\text{symm}(e) : P_2 \simeq_A[k] P_1$ is defined as the inverse CAF equivalence of e.$$

Lean4

@[deprecated "use instead `toAffineEquiv_symm`, in the reverse direction" (since := "2025-06-08")]
theorem symm_toAffineEquiv (e : P₁ ≃ᴬ[k] P₂) : e.toAffineEquiv.symm = e.symm.toAffineEquiv :=
  rfl

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