LeanPool.ErdosTuzaValtr.Main.Main

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

theorem Config.Mirror_mainGoal {γ : Type u_1} [LinearOrder γ] (C : Config γ) (n : ℕ) : C.MainGoal n → C.Mirror.MainGoal n

theorem Config.main_lemma {γ : Type u_1} [LinearOrder γ] (C : Config γ) (n : ℕ) : C.MainGoal n

theorem ErdosTuzaValtr.main {γ : Type u_1} [LinearOrder γ] (n : ℕ) (C : Config γ) (S : Finset γ) (hS : (n + 2).choose 2 + 2 ≤ S.card) : C.HasNCap 4 S ∨ C.HasNGon (n + 3) S