injective_of_source_eq_univ — Mathlib

English

If a partial equivalence e has its source equal to the whole domain, then e is injective.

Русский

Если область определения частичного эквивалента e — вся множество, то e инъективен.

LaTeX

$$$e:\\PartialEquiv\\alpha\\beta,\\quad e.\\text{source}=\\mathrm{univ} \\Rightarrow \\text{Injective}(e).$$$

Lean4

theorem injective_of_source_eq_univ (h : e.source = univ) : Injective e := by
  simpa [injective_iff_injOn_univ, h] using e.injOn

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