instPreorder — Mathlib

English

The dual of a preorder yields a preorder structure on αᵒᵈ.

Русский

Дуальный порядок задаёт структуру предорядка на αᵒᵈ.

LaTeX

$$$ \text{OrderDual.instPreorder}(\alpha) : \text{Preorder}(\alpha^{\mathrm{op}}) $$$

Lean4

instance instPreorder (α : Type*) [Preorder α] : Preorder αᵒᵈ
    where
  le_refl := fun _ ↦ le_refl _
  le_trans := fun _ _ _ hab hbc ↦ hbc.trans hab
  lt_iff_le_not_ge := fun _ _ ↦ lt_iff_le_not_ge

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