card_piFinset

Mathlib.Data.Fintype.BigOperators

URI: https://scilib.ai/kg/mathlib#Fintype.card_piFinset

English

The cardinality of piFinset over s equals the product of the cardinalities of s i.

Русский

Кардинальность piFinset над s равна произведению кардиналов каждого s(i).

LaTeX

$$$\\#(\\pi\\mathrm{Finset}\\, s) = \\prod_{i} \\#(s(i))$$$

Lean4

@[simp]
theorem card_piFinset (s : ∀ i, Finset (α i)) : #(piFinset s) = ∏ i, #(s i) := by simp [piFinset, card_map]

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

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

Разделы

Аффилиация

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