rel_iff'

Mathlib.Data.Sym.Sym2

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

English

Rel α p q holds exactly when p equals q or p equals q swapped, for p,q ∈ α×α.

Русский

Rel α p q выполняется тогда и только тогда, когда p = q или p = q.swap, для p,q ∈ α×α.

LaTeX

$$$$ \ Rel\alpha\; p\; q \;\iff\; p = q \; \lor\; p = q.swap. $$$$

Lean4

@[simp]
theorem rel_iff' {p q : α × α} : Rel α p q ↔ p = q ∨ p = q.swap := by aesop (rule_sets := [Sym2])

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

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

Разделы

Аффилиация

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