mem_pair

Mathlib.SetTheory.ZFC.PSet

URI: https://scilib.ai/kg/mathlib#PSet.mem_pair

English

An element belongs to the pair {y,z} iff it is equivalent to y or to z.

Русский

Элемент принадлежит паре {y,z} тогда и только тогда, когда он эквивалентен y или z.

LaTeX

$$$$ x \in \{ y,z \} \iff \operatorname{Equiv}(x,y) \lor \operatorname{Equiv}(x,z) $$$$

Lean4

theorem mem_pair {x y z : PSet} : x ∈ ({ y, z } : PSet) ↔ Equiv x y ∨ Equiv x z := by simp

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

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

Разделы

Аффилиация

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