vsub_card_le

Mathlib.Algebra.Group.Pointwise.Finset.Scalar

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

English

The size of s -ᵥ t is at most |s| · |t|.

Русский

Масса (размер) s -ᵥ t не больше |s| · |t|.

LaTeX

$$$ \#(s -ᵥ t) \leq \#s \cdot \#t $$$

Lean4

theorem vsub_card_le : #(s -ᵥ t : Finset α) ≤ #s * #t :=
  card_image₂_le _ _ _

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

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

Разделы

Аффилиация

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