pairwise

Mathlib.Logic.Pairwise

URI: https://scilib.ai/kg/mathlib#Subsingleton.pairwise

English

If a type α is a Subsingleton, then every relation r on α holds pairwise.

Русский

Если тип α — подсущность, тогда любое отношение r на α держится попарно.

LaTeX

$$$\\text{[Subsingleton }\\alpha]\\Rightarrow \\operatorname{Pairwise}(r)$$$

Lean4

@[simp]
protected theorem pairwise [Subsingleton α] : Pairwise r := fun _ _ h ↦ False.elim <| h.elim <| Subsingleton.elim _ _

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

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

Разделы

Аффилиация

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