card_image_iff — Mathlib

English

For any finite set S and function f, the image cardinality |f[S]| equals |S| if and only if f is injective on S.

Русский

Для конечного множества S и функции f справедливо, что |f[S]| = |S| тогда и только тогда, когда f инъективна на S.

LaTeX

$$$|f[S]| = |S| \\iff \\forall x,y \\in S,\\; f(x) = f(y) \\Rightarrow x = y$$$

Lean4

theorem card_image_iff [DecidableEq β] : #(s.image f) = #s ↔ Set.InjOn f s :=
  ⟨injOn_of_card_image_eq, card_image_of_injOn⟩

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