@[to_dual] attributes for basic types

@[reducible, inline]

abbrev DecidableLT' (α : Type u) [LT α] : Type u

DecidableLT' is equivalent to DecidableLT. It is used by @[to_dual] in order to deal with DecidableLT.

Equations

• DecidableLT' α = DecidableRel fun (a a_1 : α) => a_1 < a

@[reducible, inline]

abbrev DecidableLE' (α : Type u) [LE α] : Type u

DecidableLE' is equivalent to DecidableLE. It is used by @[to_dual] in order to deal with DecidableLE.

Equations

• DecidableLE' α = DecidableRel fun (a a_1 : α) => a_1 ≤ a

theorem le_of_eq_of_le'' {α : Type u_1} {a b c : α} [LE α] (h₁ : a = b) (h₂ : c ≤ b) : c ≤ a

theorem le_of_le_of_eq'' {α : Type u_1} {a b c : α} [LE α] (h₁ : b ≤ a) (h₂ : b = c) : c ≤ a

theorem lt_of_eq_of_lt'' {α : Type u_1} {a b c : α} [LT α] (h₁ : a = b) (h₂ : c < b) : c < a

theorem lt_of_lt_of_eq'' {α : Type u_1} {a b c : α} [LT α] (h₁ : b < a) (h₂ : b = c) : c < a