card_mul_cast_addConst

Mathlib.Combinatorics.Additive.DoublingConst

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

English

For finite A,B in G', the product of |A| with σ[A,B] equals the size of A+B: |A| · σ[A,B] = |A+B|.

Русский

Для конечных A,B в G' произведение |A| и σ[A,B] равно |A+B|.

LaTeX

$$$|A| \\cdot \\sigma[A,B] = |A+B|$$

Lean4

theorem card_mul_cast_addConst (A B : Finset G') : (#A * σ[A, B] : 𝕜) = #(A + B) := by norm_cast;
  exact card_mul_addConst _ _

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

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

Разделы

Аффилиация

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