product_singleton

Mathlib.Data.Finset.Prod

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

← MathLib Explorer

English

A singleton on each side yields a singleton pair: {a} × {b} = {(a,b)}.

Русский

Единичное множество слева и справа дают единственный элемент-пару: {a} × {b} = {(a,b)}.

LaTeX

$$$\\{a\\} \\times \\{b\\} = \\{(a,b)\\}$$$

Lean4

@[simp]
theorem product_singleton : s ×ˢ { b } = s.map ⟨fun i => (i, b), Prod.mk_left_injective _⟩ :=
  by
  ext ⟨x, y⟩
  simp [and_left_comm, eq_comm]

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

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

Разделы

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

Аффилиация

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