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]
theorem IsTotalPreorder.swap {α : Type u} (r : α → α → Prop) [IsTotalPreorder α r] :
IsTotalPreorder α (Function.swap r)
source
@[deprecated]
instance instIsTotalPreorderLe_1 {α : Type u} [LinearOrder α] :
IsTotalPreorder α fun (x1 x2 : α) => x1 ≤ x2
Equations
  • ⋯ = ⋯
source
@[deprecated]
instance instIsTotalPreorderGe {α : Type u} [LinearOrder α] :
IsTotalPreorder α fun (x1 x2 : α) => x1 ≥ x2
Equations
  • ⋯ = ⋯
source
@[deprecated]
instance instIsIncompTransLt {α : Type u} [LinearOrder α] :
IsIncompTrans α fun (x1 x2 : α) => x1 < x2
Equations
  • ⋯ = ⋯