card_diffs_le

Mathlib.Data.Finset.Sups

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

English

The cardinality of the diffs is at most the product of the cardinalities: # (s \\ t) ≤ # s · # t.

Русский

Кардинальность диффов не превосходит произведение кардинальностей s и t: #(s \\\\ t) ≤ #s · #t.

LaTeX

$$$ #(s \\\\ t) \\le #s \\cdot #t $$$

Lean4

theorem card_diffs_le : #(s \\ t) ≤ #s * #t :=
  card_image₂_le _ _ _

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

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

Разделы

Аффилиация

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