symm' — Mathlib

English

If e is equivalent to e', then their inverses are equivalent: e.symm ≈ e'.symm.

Русский

Если e эквивалентно e', то обратные отображения e.symm и e'.symm эквивалентны.

LaTeX

$$$ e \approx e' \;\Rightarrow\; e^{-1} \approx {e'}^{-1} $$$

Lean4

/-- If two open partial homeomorphisms are equivalent, so are their inverses. -/
theorem symm' {e e' : OpenPartialHomeomorph X Y} (h : e ≈ e') : e.symm ≈ e'.symm :=
  PartialEquiv.EqOnSource.symm' h

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