Note about deprecated files #
This file is deprecated, and is no longer imported by anything in mathlib other than other deprecated files, and test files. You should not need to import it.
Unbundled relation classes #
In this file we prove some properties of Is* classes defined in
Mathlib/Deprecated/AlgebraClasses.lean.
@[deprecated]
theorem
IsTotalPreorder.swap
{α : Type u}
(r : α → α → Prop)
[IsTotalPreorder α r]
:
IsTotalPreorder α (Function.swap r)
@[deprecated]
instance
instIsTotalPreorderLe_1
{α : Type u}
[LinearOrder α]
:
IsTotalPreorder α fun (x1 x2 : α) => x1 ≤ x2
@[deprecated]
instance
instIsTotalPreorderGe
{α : Type u}
[LinearOrder α]
:
IsTotalPreorder α fun (x1 x2 : α) => x1 ≥ x2
@[deprecated]
instance
instIsIncompTransLt
{α : Type u}
[LinearOrder α]
:
IsIncompTrans α fun (x1 x2 : α) => x1 < x2