card_image_of_injective

Mathlib.Data.Finset.Card

URI: https://scilib.ai/kg/mathlib#Finset.card_image_of_injective

English

If f is injective on S, then the image of S under f has the same cardinality as S.

Русский

Если f инъективна на S, то образ S при действии f имеет ту же кардинальность, что и S.

LaTeX

$$$\\text{Injective}(f|_S) \\Rightarrow |f[S]| = |S|$$$

Lean4

theorem card_image_of_injective [DecidableEq β] (s : Finset α) (H : Injective f) : #(s.image f) = #s :=
  card_image_of_injOn fun _ _ _ _ h => H h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru