toPartialEquiv — Mathlib

English

The map sending an embedding f to its partial equivalence is injective.

Русский

Отображение вложения в частичную эквивалентность инъективно.

LaTeX

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

Lean4

/-- Given an embedding, returns the corresponding partial equivalence with `⊤` as domain. -/
noncomputable def toPartialEquiv (f : M ↪[L] N) : M ≃ₚ[L] N :=
  ⟨⊤, f.toHom.range, f.equivRange.comp (Substructure.topEquiv)⟩

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