injective_codRestrict — Mathlib

English

The codRestrict map f|_S is injective iff f is injective (under appropriate membership h).

Русский

КодRestrict отображение f|_S инъективно тогда и только тогда, когда f инъективно (при соответствующем условии принадлежности).

LaTeX

$$$$ \\text{Injective}(f\\restriction S) \\;\\Leftrightarrow\\; \\text{Injective}(f) $$$$

Lean4

@[to_additive (attr := simp)]
theorem injective_codRestrict {S} [SetLike S N] [SubmonoidClass S N] (f : M →* N) (s : S) (h : ∀ x, f x ∈ s) :
    Function.Injective (f.codRestrict s h) ↔ Function.Injective f :=
  ⟨fun H _ _ hxy ↦ H <| Subtype.eq hxy, fun H _ _ hxy ↦ H (congr_arg Subtype.val hxy)⟩

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