eq_of_eqOnSource_univ — Mathlib

English

Two equivalent partial equivalences are equal when the source and target are universal.

Русский

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

LaTeX

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

Lean4

/-- Two equivalent partial equivs are equal when the source and target are `univ`. -/
theorem eq_of_eqOnSource_univ (e e' : PartialEquiv α β) (h : e ≈ e') (s : e.source = univ) (t : e.target = univ) :
    e = e' := by
  refine PartialEquiv.ext (fun x => ?_) (fun x => ?_) h.1
  · apply h.2
    rw [s]
    exact mem_univ _
  · apply h.symm'.2
    rw [symm_source, t]
    exact mem_univ _

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