isTrans_singleton

Mathlib.Data.Rel

URI: https://scilib.ai/kg/mathlib#SetRel.isTrans_singleton

English

For any pair x in α×α, the singleton relation {x} is transitive.

Русский

Для любого элемента x ∈ α×α отношение-одиночка {x} является транзитивным.

LaTeX

$$$\forall x=(a,b) \in \alpha \times \alpha, \ {x} \text{ is transitive on } \alpha$$$

Lean4

instance isTrans_singleton (x : α × α) : SetRel.IsTrans { x } where trans _ _ _ := by aesop

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

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

Разделы

Аффилиация

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