Documentation

Mathlib.Deprecated.RelClasses

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.

source
@[deprecated "No deprecation message was provided." (since := "2024-07-30")]
theorem IsTotalPreorder.swap {α : Type u} (r : α → α → Prop) [IsTotalPreorder α r] :
IsTotalPreorder α (Function.swap r)
source
@[deprecated "No deprecation message was provided." (since := "2024-08-22")]
instance instIsTotalPreorderLe_1 {α : Type u} [LinearOrder α] :
IsTotalPreorder α fun (x1 x2 : α) => x1 ≤ x2
source
@[deprecated "No deprecation message was provided." (since := "2024-08-22")]
instance instIsTotalPreorderGe {α : Type u} [LinearOrder α] :
IsTotalPreorder α fun (x1 x2 : α) => x1 ≥ x2
source
@[deprecated "No deprecation message was provided." (since := "2024-07-30")]
instance instIsIncompTransLt {α : Type u} [LinearOrder α] :
IsIncompTrans α fun (x1 x2 : α) => x1 < x2