instIsPreorder_mathlib

Mathlib.Order.Defs.PartialOrder

URI: https://scilib.ai/kg/mathlib#instIsPreorder_mathlib

English

For any preorder α, the relation ≤ is reflexive and transitive.

Русский

Для любого предпорядка α отношение ≤ рефлексивно и транзитивно.

LaTeX

$$$\forall x\, (x \le x) \land \forall x\forall y\forall z\ ((x \le y \land y \le z) \rightarrow x \le z)$$$

Lean4

instance [Preorder α] : Std.IsPreorder α where
  le_refl := Preorder.le_refl
  le_trans := Preorder.le_trans

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

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

Разделы

Аффилиация

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