instIsPreorderLe

Mathlib.Order.RelClasses

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

English

≤ forms a preorder on α: reflexive and transitive.

Русский

≤ образует предпорядок на α: рефлексивность и транзитивность.

LaTeX

$$(\\forall x : α, x ≤ x) ∧ (\\forall x,y,z : α, x ≤ y ∧ y ≤ z ⇒ x ≤ z)$$

Lean4

instance [Preorder α] : IsPreorder α (· ≤ ·) where

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

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

Разделы

Аффилиация

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