rel_iff

Mathlib.Data.Sym.Sym2

URI: https://scilib.ai/kg/mathlib#Sym2.rel_iff

English

For x,y,z,w ∈ α, Rel α (x,y) (z,w) holds exactly when either (x=z and y=w) or (x=w and y=z).

Русский

Для x,y,z,w ∈ α отношение Rel α между (x,y) и (z,w) эквивалентно либо (x=z и y=w), либо (x=w и y=z).

LaTeX

$$$$ \ Rel\alpha\; (x,y)\; (z,w) \iff (x=z \land y=w) \lor (x=w \land y=z). $$$$

Lean4

theorem rel_iff {x y z w : α} : Rel α (x, y) (z, w) ↔ x = z ∧ y = w ∨ x = w ∧ y = z := by simp

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

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

Разделы

Аффилиация

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