LeanPool.ErdosTuzaValtr.Main.Lemmas.JoinN2N3N2 #
Imported Lean Pool material for LeanPool.ErdosTuzaValtr.Main.Lemmas.JoinN2N3N2.
theorem
Config.join_n2_n3_n2_ff
{α : Type u_1}
[LinearOrder α]
(C : Config α)
(S : Finset α)
(_cap4_free : ¬C.HasNCap 4 S)
{n : ℕ}
(x y : α)
{P : List α}
(hPx : C.NCup (n + 2) (P ++ [x]))
(Px_in_S : (P ++ [x]).In S)
{Q : List α}
(hxQy : C.NCup (n + 3) (x :: Q ++ [y]))
(xQy_in_S : (x :: Q ++ [y]).In S)
{R : List α}
(hyR : C.NCup (n + 2) (y :: R))
(yR_in_S : (y :: R).In S)
(label : C.Label S)
(sxy : ¬label.Slope x y)
:
∃ (p : α) (q : α) (r : α) (s : α), C.HasInterweavedLaced (n + 3) S p q r s
theorem
Config.join_n2_n3_n2_tt
{α : Type u_1}
[LinearOrder α]
(C : Config α)
(S : Finset α)
(cap4_free : ¬C.HasNCap 4 S)
{n : ℕ}
(x y : α)
{P : List α}
(hPx : C.NCup (n + 2) (P ++ [x]))
(Px_in_S : (P ++ [x]).In S)
{Q : List α}
(hxQy : C.NCup (n + 3) (x :: Q ++ [y]))
(xQy_in_S : (x :: Q ++ [y]).In S)
{R : List α}
(hyR : C.NCup (n + 2) (y :: R))
(yR_in_S : (y :: R).In S)
(label : C.Label S)
(sxy : label.Slope x y)
:
∃ (p : α) (q : α) (r : α) (s : α), C.HasInterweavedLaced (n + 3) S p q r s
theorem
Config.join_n2_n3_n2
{α : 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_ncup : C.NCup (n + 2) cx)
(cx_in_S : cx.In S)
{c : List α}
(c_ncup : C.NCup (n + 3) c)
(c_in_S : c.In S)
{cy : List α}
(cy_ncup : C.NCup (n + 2) cy)
(cy_in_S : cy.In S)
(x : α)
(hxcx : x ∈ cx.getLast?)
(hxc : x ∈ c.head?)
(y : α)
(hyc : y ∈ c.getLast?)
(hycy : y ∈ cy.head?)
:
∃ (p : α) (q : α) (r : α) (s : α), C.HasInterweavedLaced (n + 3) S p q r s