convolution_le_card_right

Mathlib.Combinatorics.Additive.Convolution

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

← MathLib Explorer

English

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

Русский

Для конечных A,B ⊆ G и x ∈ G, (A * B)(x) ≤ |A|.

LaTeX

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

Lean4

@[to_additive addConvolution_le_card_right]
theorem convolution_le_card_right : A.convolution B x ≤ #B :=
  by
  rw [← inv_inv B, ← inv_inv x, ← card_smul_inter, card_inv]
  exact card_le_card inter_subset_right

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

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

Разделы

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

Аффилиация

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