prod_singleton

Mathlib.Data.Set.Prod

URI: https://scilib.ai/kg/mathlib#Set.prod_singleton

English

The product s × {b} equals { (x, b) : x ∈ s }.

Русский

Произведение s на {b} равно { (x, b) : x ∈ s }.

LaTeX

$$$ s \times \{b\} = \{ (x, b) : x \in s \}$$$

Lean4

theorem prod_singleton : s ×ˢ ({ b } : Set β) = (fun a => (a, b)) '' s :=
  by
  ext ⟨x, y⟩
  simp [and_left_comm, eq_comm]

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

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

Разделы

Аффилиация

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