LeanPool.ErdosTuzaValtr.Main.Lemmas.InterweavedLacedNgon

Imported Lean Pool material for LeanPool.ErdosTuzaValtr.Main.Lemmas.InterweavedLacedNgon.

theorem Config.hasInterweavedLaced_hasNGon_ff {α : Type u_1} [LinearOrder α] (C : Config α) {n : ℕ} {S : Finset α} (cap4_free : ¬C.HasNCap 4 S) {p q r s : α} (label : C.Label S) (q_lt_r : q < r) (sqr : ¬label.Slope q r) : C.HasInterweavedLaced (n + 2) S p q r s → C.HasNGon (n + 3) S

theorem Config.hasInterweavedLaced_hasNGon_tt {α : Type u_1} [LinearOrder α] (C : Config α) {n : ℕ} {S : Finset α} (cap4_free : ¬C.HasNCap 4 S) {p q r s : α} (label : C.Label S) (q_lt_r : q < r) (sqr : label.Slope q r) : C.HasInterweavedLaced (n + 2) S p q r s → C.HasNGon (n + 3) S

theorem Config.hasInterweavedLaced_hasNGon {α : Type u_1} [LinearOrder α] (C : Config α) {n : ℕ} {S : Finset α} (cap4_free : ¬C.HasNCap 4 S) {p q r s : α} : C.HasInterweavedLaced (n + 2) S p q r s → C.HasNGon (n + 3) S