symm_toPartialEquiv — Mathlib

English

The inverse's underlying partial equivalence equals the inverse of the original's underlying partial equivalence.

Русский

Базовая частичная эквивалентность обратного отображения равна обратной частичной эквивалентности исходного.

LaTeX

$$$e.symm.toPartialEquiv = e.toPartialEquiv.symm$$$

Lean4

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

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