injective_iff_injOn_univ — Mathlib

English

Let f : α → β. Then f is injective on the whole domain if and only if f is injective on univ.

Русский

Пусть f : α → β. Тогда f инъективна на всей области определения тогда и только тогда, когда она инъективна на univ.

LaTeX

$$$ \\operatorname{Injective}(f) \\iff \\operatorname{InjOn} f \\mathrm{univ}$$$

Lean4

theorem injective_iff_injOn_univ : Injective f ↔ InjOn f univ :=
  ⟨fun h _ _ _ _ hxy => h hxy, fun h _ _ heq => h trivial trivial heq⟩

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