mk_mem_prod

Mathlib.Data.Set.Operations

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

English

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

Русский

Если ha: a ∈ s и hb: b ∈ t, тогда (a,b) ∈ s ×ˢ t.

LaTeX

$$$$ha: a \\in s \\;\\land\\; hb: b \\in t \\;\\Rightarrow\\; (a,b) \\in s \\timesˢ t.$$$$

Lean4

theorem mk_mem_prod (ha : a ∈ s) (hb : b ∈ t) : (a, b) ∈ s ×ˢ t :=
  ⟨ha, hb⟩

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

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

Разделы

Аффилиация

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