card_div_le

Mathlib.Algebra.Group.Pointwise.Finset.Basic

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

English

The number of elements in s / t is at most |s| · |t|.

Русский

Число элементов в s / t не превосходит |s| · |t|.

LaTeX

$$$|s / t| \\le |s| \\cdot |t|$$$

Lean4

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

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

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

Разделы

Аффилиация

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