restrict_injective — Mathlib

English

If f is injective, then its restriction to a subset p is injective.

Русский

Если f инъективно отображает, то его ограничение на множество p тоже инъективно.

LaTeX

$$$$\forall \alpha \beta (f: \alpha \to \beta) (p: \alpha \to \mathrm{Prop}), \ \mathrm{Injective} f \Rightarrow \mathrm{Injective}(\mathrm{restrict}\ p\, f).$$$$

Lean4

theorem restrict_injective {α β} {f : α → β} (p : α → Prop) (h : Injective f) : Injective (restrict p f) :=
  h.comp coe_injective

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