toPartialEquiv_injective — Mathlib

English

The embedding-to-partial-equivalence map is injective; equivalently, two embeddings yield the same partial equivalence only if they are identical.

Русский

Включение в частичную эквивалентность инъективно; если две вложенности дают одинаковую частичную эквивалентность, они совпадают.

LaTeX

$$$\forall f,g : M \hookrightarrow N,\; f^{\mathrm{toPartialEquiv}} = g^{\mathrm{toPartialEquiv}} \Rightarrow f=g.$$$

Lean4

theorem toPartialEquiv_injective : Function.Injective (fun f : M ↪[L] N ↦ f.toPartialEquiv) :=
  by
  intro _ _ h
  ext
  rw [PartialEquiv.ext_iff] at h
  rcases h with ⟨_, H⟩
  exact H _ (Substructure.mem_top _)

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