injective_codRestrict — Mathlib

English

The restriction of f to S is injective if and only if f is injective.

Русский

Ограничение f до S инъективно тогда и только тогда, когда f инъективен.

LaTeX

$$$ \mathrm{Injective} \bigl(f.\mathrm{codRestrict} S hf\bigr) \iff \mathrm{Injective}(f)$$

Lean4

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

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