card_mul_le

Mathlib.Algebra.Group.Pointwise.Finset.Basic

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

English

The cardinality of s*t is at most the product of the cardinalities: |s*t| ≤ |s|·|t|.

Русский

Кардинальность s*t не превышает произведения кардинальностей |s|·|t|.

LaTeX

$$$|s * t| \le |s| \cdot |t|$$$

Lean4

@[to_additive]
theorem card_mul_le : #(s * t) ≤ #s * #t :=
  card_image₂_le _ _ _

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

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

Разделы

Аффилиация

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