mem_prod

Mathlib.SetTheory.ZFC.Basic

URI: https://scilib.ai/kg/mathlib#ZFSet.mem_prod

English

z ∈ prod x y iff ∃ a ∈ x, ∃ b ∈ y, z = pair a b.

Русский

z принадлежит произведению x × y тогда и только тогда, когда существует a ∈ x и b ∈ y такие, что z = pair a b.

LaTeX

$$$z \\in x \\times y \\iff \\exists a \\in x, \\exists b \\in y, z = a.pair b$$$

Lean4

@[simp]
theorem mem_prod {x y z : ZFSet.{u}} : z ∈ prod x y ↔ ∃ a ∈ x, ∃ b ∈ y, z = pair a b := by simp [prod]

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

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

Разделы

Аффилиация

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