injective_iff_pairwise_ne — Mathlib

English

Injectivity of f is equivalent to pairwise inequality of f on distinct inputs.

Русский

Инъективность функции f эквивалентна попаренной неравности на разных входах.

LaTeX

$$$\\operatorname{Injective}(f) \\iff \\operatorname{Pairwise}\\bigl( (\\neq) \\text{ on } f \\bigr)$$$

Lean4

theorem injective_iff_pairwise_ne : Injective f ↔ Pairwise ((· ≠ ·) on f) :=
  forall₂_congr fun _i _j => not_imp_not.symm

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