injective_codRestrict — Mathlib

English

A variant equivalence for injectivity of codRestrict and f in the star-algebra setting.

Русский

Вариант эквивалентности инъективности codRestrict и f в контексте звездной алгебры.

LaTeX

$$$\\mathrm{Injective}(\\mathrm{instFunLike}.coe (\\mathrm{codRestrict}\\ f\\ S\\ hf)) \\iff \\mathrm{Injective}(f).$$$

Lean4

theorem injective_codRestrict (f : F) (S : NonUnitalStarSubalgebra R B) (hf : ∀ x : A, f x ∈ S) :
    Function.Injective (NonUnitalStarAlgHom.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 :)⟩

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