LeanPool.ErdosTuzaValtr.Etv.Defs

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

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

p and q are laced of order n in S: an n-cup from p to q extends on both sides to cups whose lengths sum to n.

Equations

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

theorem Config.HasLaced.mem_ends {α : Type u_1} [LinearOrder α] {C : Config α} {n : ℕ} {S : Finset α} {p q : α} (h : C.HasLaced n S p q) : p ∈ S ∧ q ∈ S

def Config.HasInterweavedLaced {α : Type u_1} [LinearOrder α] (C : Config α) (n : ℕ) (S : Finset α) (p q r s : α) : Prop

Two interweaving laced pairs (p, r) and (q, s) with p < q ≤ r < s.

Equations

• C.HasInterweavedLaced n S p q r s = ((p < q ∧ q ≤ r ∧ r < s) ∧ C.HasLaced n S p r ∧ C.HasLaced n S q s)

def Config.HasJoin {α : Type u_1} [LinearOrder α] (C : Config α) (a b : ℕ) (S : Finset α) : Prop

A join of an a-cup and a b-cup in S meeting at a common point p.

Equations

• C.HasJoin a b S = ∃ (p : α) (cl : List α) (cr : List α), (C.NCup a cl ∧ cl.In S ∧ p ∈ cl.getLast?) ∧ C.NCup b cr ∧ cr.In S ∧ p ∈ cr.head?