instLawfulOrderLT_mathlib — Mathlib

English

Given a preorder, there is a canonical strict order < defined by x < y iff x ≤ y and not y ≤ x.

Русский

Пусть задано предпорядок; существует каноническое строгое отношение < такое, что x < y тогда и только тогда, когда x ≤ y и не y ≤ x.

LaTeX

$$$\mathrm{Std.LawfulOrderLT}(\alpha)$$$

Lean4

instance [Preorder α] : Std.LawfulOrderLT α where lt_iff := Preorder.lt_iff_le_not_ge

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