convolution_le_card_left

Mathlib.Combinatorics.Additive.Convolution

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

← MathLib Explorer

English

For finite A,B ⊆ G and any x, (A * B)(x) ≤ |B|.

Русский

Для любых конечных A,B ⊆ G и любого x выполняется (A * B)(x) ≤ |B|.

LaTeX

$$$ (A * B)(x) \le |B| $$$

Lean4

@[to_additive addConvolution_le_card_left]
theorem convolution_le_card_left : A.convolution B x ≤ #A :=
  by
  rw [← inv_inv B, ← card_inter_smul]
  exact card_le_card inter_subset_left

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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