injOn_iff_pairwise_ne — Mathlib

English

Let f: ι → α and s ⊆ ι. f is injective on s if and only if the values f x for x in s are pairwise distinct; equivalently, for all x,y in s with x ≠ y we have f x ≠ f y.

Русский

Пусть f: ι → α и S ⊆ ι. Инъективность f на S эквивалентна тому, что значения f(x) для x∈S различны попарно; то есть для любых x,y∈S с x≠y выполняется f(x) ≠ f(y).

LaTeX

$$$\\operatorname{InjOn}(f,s) \\iff \\forall x \\in s, \\forall y \\in s, x \\neq y \\Rightarrow f x \\neq f y$$$

Lean4

/-- See also `Function.injective_iff_pairwise_ne` -/
theorem injOn_iff_pairwise_ne {s : Set ι} : InjOn f s ↔ s.Pairwise (f · ≠ f ·) := by
  simp only [InjOn, Set.Pairwise, not_imp_not]

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