LeanPool.ErdosTuzaValtr.Main.Defs

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

def Config.MainGoal {α : Type u_1} [LinearOrder α] (C : Config α) (n : ℕ) : Prop

The configuration-relative main goal at level n: any large cap-free, cup-free finset contains an interweaved laced configuration.

Equations

• C.MainGoal n = ∀ (S : Finset α), (n + 2).choose 2 + 2 ≤ S.card → ¬C.HasNCap 4 S → ¬C.HasNCup (n + 3) S → ∃ (p : α) (q : α) (r : α) (s : α), C.HasInterweavedLaced (n + 2) S p q r s

def Config.MainGoalWlog {α : Type u_1} [LinearOrder α] (C : Config α) (n : ℕ) : Prop

The main goal under the without-loss-of-generality assumption that a certain join is absent.

Equations

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