LeanPool.ErdosTuzaValtr.Lib.Core.Rel3

Imported Lean Pool material for LeanPool.ErdosTuzaValtr.Lib.Core.Rel3.

def Mirror2 {α : Type u} {β : Sort v} (f : α → α → β) : αᵒᵈ → αᵒᵈ → β

Mirror a binary relation/function to the order dual, swapping argument order.

Equations

• Mirror2 f a b = f (OrderDual.ofDual b) (OrderDual.ofDual a)

def Mirror3 {α : Type u} {β : Sort v} (f : α → α → α → β) : αᵒᵈ → αᵒᵈ → αᵒᵈ → β

Mirror a ternary relation/function to the order dual, reversing argument order.

Equations

• Mirror3 f a b c = f (OrderDual.ofDual c) (OrderDual.ofDual b) (OrderDual.ofDual a)

@[reducible]

def DecidableRel3 {α : Sort u} (r : α → α → α → Prop) : Sort (max 1 u)

Decidability of a ternary relation: each instance is decidable.

Equations

• DecidableRel3 r = ((a b c : α) → Decidable (r a b c))

@[reducible]

def DecidableRel.Mirror2 {α : Type u} {r : α → α → Prop} (dec : DecidableRel r) : DecidableRel (_root_.Mirror2 r)

Transport decidability of a binary relation to its mirror.

Equations

• dec.Mirror2 a b = dec (OrderDual.ofDual b) (OrderDual.ofDual a)

@[reducible]

def DecidableRel3.Mirror3 {α : Type u} {r : α → α → α → Prop} (dec : DecidableRel3 r) : DecidableRel3 (_root_.Mirror3 r)

Transport decidability of a ternary relation to its mirror.

Equations

• dec.Mirror3 a b c = dec (OrderDual.ofDual c) (OrderDual.ofDual b) (OrderDual.ofDual a)