injective_codRestrict — Mathlib

English

Injectivity of codRestrict is equivalent to injectivity of the original f.

Русский

Инъективность codRestrict эквивалентна инъективности исходного f.

LaTeX

$$$ \\text{Injective} (\\mathrm{codRestrict} f S hf) \\quad\\Longleftrightarrow\\quad \\text{Injective} f $$$

Lean4

theorem injective_codRestrict (f : A →⋆ₐ[R] B) (S : StarSubalgebra R B) (hf : ∀ x : A, f x ∈ S) :
    Function.Injective (StarAlgHom.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 :)⟩

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