product_union

Mathlib.Data.Finset.Prod

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

English

The product distributes over union: s × (t ∪ t') = (s × t) ∪ (s × t').

Русский

Произведение распределяется по объединению: s × (t ∪ t') = (s × t) ∪ (s × t').

LaTeX

$$$s \\times (t \\cup t') = (s \\times t) \\cup (s \\times t')$$$

Lean4

@[simp]
theorem product_union [DecidableEq α] [DecidableEq β] : s ×ˢ (t ∪ t') = s ×ˢ t ∪ s ×ˢ t' := by grind

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

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

Разделы

Аффилиация

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