self_trans_symm — Mathlib

English

If two equivalent partial equivalences have universal source and universal target, they are equal.

Русский

Если две эквивалентные частичные эквивалентности имеют универсальные источник и целевой домен, они равны.

LaTeX

$$$ e \\approx e' \\land e.source = \\univ \\land e.target = \\univ \\Rightarrow e = e' $$$

Lean4

/-- Composition of a partial equivalence and its inverse is equivalent to
the restriction of the identity to the source. -/
theorem self_trans_symm : e.trans e.symm ≈ ofSet e.source :=
  by
  have A : (e.trans e.symm).source = e.source := by mfld_set_tac
  refine ⟨by rw [A, ofSet_source], fun x hx => ?_⟩
  rw [A] at hx
  simp only [hx, mfld_simps]

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