symm_eqOn — Mathlib

English

Two equivalent partial equivalences have their inverses equal on the target.

Русский

Две эквивалентные частичные эквивалентности имеют совпадающие обратные функции на целевой области.

LaTeX

$$EqOn e.symm e'.symm e.target$$

Lean4

/-- Two equivalent partial equivs have coinciding inverses on the target. -/
theorem symm_eqOn {e e' : PartialEquiv α β} (h : e ≈ e') : EqOn e.symm e'.symm e.target :=
  eqOn h.symm'

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