symm_toPartialEquiv — Mathlib

English

The symmetry of an equivalence, when translated to a PartialEquiv, equals the symmetry of the corresponding PartialEquiv.

Русский

Обратная эквивалентности переводится в PartialEquiv так, что её симметрия равна симметрии соответствующего PartialEquiv.

LaTeX

$$$\\text{theorem }\\mathrm{symm_toPartialEquiv} : e^{\\mathrm{symm}}.\\mathrm{toPartialEquiv} = e.\\mathrm{toPartialEquiv}.\\mathrm{symm}$$$

Lean4

@[simp, mfld_simps]
theorem symm_toPartialEquiv : e.symm.toPartialEquiv = e.toPartialEquiv.symm :=
  rfl

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