symm' — Mathlib

English

If two partial equivalences are equivalent, then their inverses are equivalent.

Русский

Если две частичные эквивалентности эквивалентны, то их инверсные эквивалентности тоже эквивалентны.

LaTeX

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

Lean4

/-- If two partial equivs are equivalent, so are their inverses. -/
theorem symm' {e e' : PartialEquiv α β} (h : e ≈ e') : e.symm ≈ e'.symm :=
  by
  refine ⟨target_eq h, eqOn_of_leftInvOn_of_rightInvOn e.leftInvOn ?_ ?_⟩ <;>
    simp only [symm_source, target_eq h, source_eq h, e'.symm_mapsTo]
  exact e'.rightInvOn.congr_right e'.symm_mapsTo (source_eq h ▸ h.eqOn.symm)

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