triplewise_triple

Mathlib.Data.List.Triplewise

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

English

The triplewise relation on a triple [a,b,c] is equivalent to the ternary predicate p on (a,b,c).

Русский

Тройная связь Triplewise на тройке [a,b,c] эквивалентна тройному предикату p на (a,b,c).

LaTeX

$$$$ [a,b,c].Triplewise\\, p \\iff p\\,a\\,b\\,c. $$$$

Lean4

@[simp]
theorem triplewise_triple : [a, b, c].Triplewise p ↔ p a b c := by simp [triplewise_cons]

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

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

Разделы

Аффилиация

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