product_empty

Mathlib.Data.Finset.Prod

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

← MathLib Explorer

English

The Cartesian product of any Finset with the empty set is empty.

Русский

Декартово произведение любого множества с пустым множеством пусто.

LaTeX

$$$(s \\\\times ∅) = ∅$$$

Lean4

@[simp]
theorem product_empty (s : Finset α) : s ×ˢ (∅ : Finset β) = ∅ :=
  eq_empty_of_forall_notMem fun _ h => notMem_empty _ (Finset.mem_product.1 h).2

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

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

Разделы

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

Аффилиация

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