LeanPool.ErdosTuzaValtr.Lib.List.Defs

Imported Lean Pool material for LeanPool.ErdosTuzaValtr.Lib.List.Defs.

def List.In {α : Type u_1} (l : List α) (S : Finset α) : Prop

Local notion for a list whose elements all lie in a finset.

Equations

• l.In S = ∀ a ∈ l, a ∈ S

def Finset.Mirror {α : Type u_1} [LinearOrder α] (S : Finset α) : Finset αᵒᵈ

The image of a finset under the order-dual embedding.

Equations

• S.Mirror = Finset.image (⇑OrderDual.toDual) S

def Finset.ofMirror {α : Type u_1} [LinearOrder α] (S : Finset αᵒᵈ) : Finset α

The image of a finset of order-dual elements back under ofDual.

Equations

• S.ofMirror = Finset.image (⇑OrderDual.ofDual) S

def List.Mirror {α : Type u_1} (l : List α) : List αᵒᵈ

Flip a list of elements together with its order, landing in the order dual.

Equations

• l.Mirror = (List.map (⇑OrderDual.toDual) l).reverse

def List.ofMirror {α : Type u_1} (l : List αᵒᵈ) : List α

Recover a list from its mirror in the order dual.

Equations

• l.ofMirror = (List.map (⇑OrderDual.ofDual) l).reverse

inductive List.Chain3 {α : Type u_1} (R : α → α → α → Prop) : α → α → List α → Prop

Chain3 R a b l means R holds for every three consecutive entries of a :: b :: l.

• nil {α : Type u_1} {R : α → α → α → Prop} {a b : α} : Chain3 R a b []
• cons {α : Type u_1} {R : α → α → α → Prop} {a b c : α} {l : List α} : R a b c → Chain3 R b c l → Chain3 R a b (c :: l)

def List.Chain3' {α : Type u_1} (R : α → α → α → Prop) : List α → Prop

Chain3' R l means R holds for every three consecutive entries of l.

Equations

• List.Chain3' R [] = True
• List.Chain3' R [head] = True
• List.Chain3' R (a :: b :: l) = List.Chain3 R a b l

@[simp]

theorem List.chain3_cons {α : Type u_1} {R : α → α → α → Prop} {a b c : α} {l : List α} : Chain3 R a b (c :: l) ↔ R a b c ∧ Chain3 R b c l

@[simp]

theorem List.chain3_nil {α : Type u_1} {R : α → α → α → Prop} {a b : α} : Chain3 R a b []

@[implicit_reducible]

instance List.decidableChain3 {α : Type u_1} {R : α → α → α → Prop} [DecidableRel3 R] (a b : α) (l : List α) : Decidable (Chain3 R a b l)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance List.decidableChain3' {α : Type u_1} {R : α → α → α → Prop} [DecidableRel3 R] (l : List α) : Decidable (Chain3' R l)

Equations

• l.decidableChain3' = List.casesOn l instDecidableTrue fun (a : α) (tail : List α) => List.casesOn tail instDecidableTrue fun (b : α) (l : List α) => List.decidableChain3 a b l