extendDomainHom_injective — Mathlib

English

ExtendDomainHom is injective: if extendDomainHom f(e) = extendDomainHom f(e'), then e = e'.

Русский

ExtendDomainHom инъективен: если extendDomainHom f(e) = extendDomainHom f(e'), то e = e'.

LaTeX

$$$\text{ExtendDomainHom}_{f} \text{ is injective}$$$

Lean4

theorem extendDomainHom_injective : Function.Injective (extendDomainHom f) :=
  (injective_iff_map_eq_one (extendDomainHom f)).mpr fun e he =>
    ext fun x => f.injective <| Subtype.ext ((extendDomain_apply_image e f x).symm.trans (Perm.ext_iff.mp he (f x)))

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