LeanPool.ErdosTuzaValtr.Main.Lemmas.JoinN2N3JoinN3N2 #
Imported Lean Pool material for LeanPool.ErdosTuzaValtr.Main.Lemmas.JoinN2N3JoinN3N2.
theorem
Config.join_n2_n2_interweaved
{α : Type u_1}
[LinearOrder α]
(C : Config α)
{S : Finset α}
{n : ℕ}
{c1 : List α}
(c1_cup : C.NCup (n + 2) c1)
(c1_in_S : c1.In S)
{c2 : List α}
(c2_cup : C.NCup (n + 2) c2)
(c2_in_S : c2.In S)
(x : α)
(c1_last : x ∈ c1.getLast?)
(c2_head : x ∈ c2.head?)
:
∃ (p : α) (q : α) (r : α) (s : α), C.HasInterweavedLaced (n + 2) S p q r s
theorem
Config.join_n2_n3_join_n3_n2_main
{α : Type u_1}
[LinearOrder α]
(C : Config α)
(S : Finset α)
(n : ℕ)
(cap4_free : ¬C.HasNCap 4 S)
(cup_free : ¬C.HasNCup (n + 4) S)
{cx : List α}
(cx_cup : C.NCup (n + 2) cx)
(cx_in_S : cx.In S)
{cx1 : List α}
(cx1_cup : C.NCup (n + 3) cx1)
(cx1_in_S : cx1.In S)
{cy1 : List α}
(cy1_cup : C.NCup (n + 3) cy1)
(cy1_in_S : cy1.In S)
{cy : List α}
(cy_cup : C.NCup (n + 2) cy)
(cy_in_S : cy.In S)
(x : α)
(cx_last : x ∈ cx.getLast?)
(cx1_head : x ∈ cx1.head?)
(y : α)
(cy1_last : y ∈ cy1.getLast?)
(cy_head : y ∈ cy.head?)
:
∃ (p : α) (q : α) (r : α) (s : α), C.HasInterweavedLaced (n + 3) S p q r s
theorem
Config.join_n2_n3_join_n3_n2
{α : Type u_1}
[LinearOrder α]
(C : Config α)
(S : Finset α)
(n : ℕ)
(cap4_free : ¬C.HasNCap 4 S)
(cup_free : ¬C.HasNCup (n + 4) S)
(hx : C.HasJoin (n + 2) (n + 3) S)
(hy : C.HasJoin (n + 3) (n + 2) S)
:
∃ (p : α) (q : α) (r : α) (s : α), C.HasInterweavedLaced (n + 3) S p q r s