instIsPreorderGe

Mathlib.Order.RelClasses

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

English

≥ forms a preorder on α: reflexive and transitive.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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