isChain_pair

Mathlib.Data.List.Chain

URI: https://scilib.ai/kg/mathlib#List.isChain_pair

English

For any x,y, IsChain R [x,y] holds iff R x y.

Русский

Для любых x,y, IsChain R [x,y] равно R x y.

LaTeX

$$$IsChain\\;R\\;[x,y] \\iff R\\,x\\,y$$$

Lean4

theorem isChain_pair {x y} : IsChain R [x, y] ↔ R x y := by simp only [IsChain.singleton, isChain_cons_cons, and_true]

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

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

Разделы

Аффилиация

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