LeanPool.ErdosTuzaValtr.Config.Defs

Imported Lean Pool material for LeanPool.ErdosTuzaValtr.Config.Defs.

structure Config (α : Type u_1) [LinearOrder α] : Type u_1

A configuration: a decidable ternary "cup" relation on a linearly ordered type.

• Cup3 : α → α → α → Prop

  The ternary cup relation of the configuration.

• DecidableCup3 : DecidableRel3 self.Cup3

  The cup relation is decidable.

def Config.Cap3 {α : Type u_1} [ord : LinearOrder α] (C : Config α) (a b c : α) : Prop

The 3-cap relation is the negation of the 3-cup relation.

Equations

• C.Cap3 a b c = ¬C.Cup3 a b c

@[reducible]

instance Config.DecidableCap3 {α : Type u_1} [ord : LinearOrder α] (C : Config α) : DecidableRel3 C.Cap3

The 3-cap relation is decidable.

Equations

• C.DecidableCap3 a b c = instDecidableNot

def Config.Cap {α : Type u_1} [ord : LinearOrder α] (C : Config α) (l : List α) : Prop

A cap is a strictly increasing list whose consecutive triples are 3-caps.

Equations

• C.Cap l = (List.IsChain (fun (x1 x2 : α) => x1 < x2) l ∧ List.Chain3' C.Cap3 l)

def Config.Cup {α : Type u_1} [ord : LinearOrder α] (C : Config α) (l : List α) : Prop

A cup is a strictly increasing list whose consecutive triples are 3-cups.

Equations

• C.Cup l = (List.IsChain (fun (x1 x2 : α) => x1 < x2) l ∧ List.Chain3' C.Cup3 l)

def Config.Gon {α : Type u_1} [ord : LinearOrder α] (C : Config α) (l1 l2 : List α) : Prop

A gon is a cap and a cup of length at least 2 sharing their first and last endpoints.

Equations

• C.Gon l1 l2 = (2 ≤ l1.length ∧ C.Cap l1 ∧ 2 ≤ l2.length ∧ C.Cup l2 ∧ l1.head? = l2.head? ∧ l1.getLast? = l2.getLast?)

@[implicit_reducible]

instance Config.DecidableCup {α : Type u_1} [ord : LinearOrder α] (C : Config α) {l : List α} : Decidable (C.Cup l)

Equations

• C.DecidableCup = ⋯.mpr inferInstance

def Config.NCap {α : Type u_1} [ord : LinearOrder α] (C : Config α) (n : ℕ) (l : List α) : Prop

An n-cap is a cap of length n.

Equations

• C.NCap n l = (C.Cap l ∧ l.length = n)

def Config.NCup {α : Type u_1} [ord : LinearOrder α] (C : Config α) (n : ℕ) (l : List α) : Prop

An n-cup is a cup of length n.

Equations

• C.NCup n l = (C.Cup l ∧ l.length = n)

def Config.NGon {α : Type u_1} [ord : LinearOrder α] (C : Config α) (n : ℕ) (l1 l2 : List α) : Prop

An n-gon is a gon whose cap and cup lengths sum to n + 2.

Equations

• C.NGon n l1 l2 = (C.Gon l1 l2 ∧ l1.length + l2.length = n + 2)

def Config.HasNCap {α : Type u_1} [ord : LinearOrder α] (C : Config α) (n : ℕ) (S : Finset α) : Prop

A finset has an n-cap if some n-cap lies inside it.

Equations

• C.HasNCap n S = ∃ (l : List α), C.NCap n l ∧ l.In S

def Config.HasNCup {α : Type u_1} [ord : LinearOrder α] (C : Config α) (n : ℕ) (S : Finset α) : Prop

A finset has an n-cup if some n-cup lies inside it.

Equations

• C.HasNCup n S = ∃ (l : List α), C.NCup n l ∧ l.In S

def Config.HasNGon {α : Type u_1} [ord : LinearOrder α] (C : Config α) (n : ℕ) (S : Finset α) : Prop

A finset has an n-gon if some n-gon lies inside it.

Equations

• C.HasNGon n S = ∃ (l1 : List α) (l2 : List α), C.NGon n l1 l2 ∧ l1.In S ∧ l2.In S