injective_codRestrict — Mathlib

English

CodRestrict preserves injectivity: codRestrict f s h is injective iff f is injective.

Русский

CodRestrict сохраняет вводимость: инъективность codRestrict равна инъективности f.

LaTeX

$$$\\text{Injective }(codRestrict f s h) \\;\\Longleftrightarrow\\; \\text{Injective } f$$$

Lean4

@[simp]
theorem injective_codRestrict {f : ι → α} {s : Set α} (h : ∀ x, f x ∈ s) :
    Injective (codRestrict f s h) ↔ Injective f := by simp only [Injective, Subtype.ext_iff, val_codRestrict_apply]

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