mk_mem_product

Mathlib.Data.Finset.Prod

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

English

If a ∈ s and b ∈ t, then (a,b) ∈ s ×ˢ t.

Русский

Если a ∈ s и b ∈ t, то (a,b) ∈ s ×ˢ t.

LaTeX

$$$a \in s \;\land\; b \in t \;\Rightarrow\; (a,b) \in s ×ˢ t$$$

Lean4

theorem mk_mem_product (ha : a ∈ s) (hb : b ∈ t) : (a, b) ∈ s ×ˢ t :=
  mem_product.2 ⟨ha, hb⟩

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

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

Разделы

Аффилиация

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