injective_codRestrict — Mathlib

English

An abbreviation to restrict the codomain of a nonunital AlgHom to its range.

Русский

Сокращение кодомпозитора до образа.

LaTeX

$$$\\mathrm{rangeRestrict}(f) : A \\to B$ with codomain restricted to $\\mathrm{range}(f)$$$

Lean4

theorem injective_codRestrict (f : F) (S : NonUnitalSubalgebra R B) (hf : ∀ x : A, f x ∈ S) :
    Function.Injective (NonUnitalAlgHom.codRestrict f S hf) ↔ Function.Injective f :=
  ⟨fun H _x _y hxy => H <| Subtype.eq hxy, fun H _x _y hxy => H (congr_arg Subtype.val hxy :)⟩

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