LeanPool.ErdosTuzaValtr.Etv.Label

Imported Lean Pool material for LeanPool.ErdosTuzaValtr.Etv.Label.

structure Config.Label {α : Type u_1} [LinearOrder α] (C : Config α) (S : Finset α) : Type u_1

A labeling of the edges of S by a slope predicate compatible with the cup relation.

• Slope : α → α → Prop

  The slope predicate assigning a direction to each ordered edge.

• extend_left {a b : α} : a ∈ S → b ∈ S → a < b → ¬self.Slope a b → ∀ {c : α}, c ∈ S → b < c → C.Cup3 a b c

  An edge of negative slope extends to the left into a 3-cup.

• extend_right {a b : α} : a ∈ S → b ∈ S → a < b → self.Slope a b → ∀ {c : α}, c ∈ S → c < a → C.Cup3 c a b

  An edge of positive slope extends to the right into a 3-cup.

def Cap4FreeSlope {α : Type u_1} [LinearOrder α] (C : Config α) (S : Finset α) (a b : α) : Prop

The canonical slope on a finset: a, b has this slope when every earlier point forms a 3-cup with a, b.

Equations

• Cap4FreeSlope C S a b = ∀ (c : ↥S), ↑c < a → C.Cup3 (↑c) a b

@[implicit_reducible]

instance decidableCap4FreeSlope {α : Type u_1} [LinearOrder α] (C : Config α) (S : Finset α) : DecidableRel (Cap4FreeSlope C S)

Equations

• decidableCap4FreeSlope C S a b = ⋯.mpr (⋯.mpr inferInstance)

def cap4FreeLabel {α : Type u_1} [LinearOrder α] {C : Config α} {S : Finset α} (h : ¬C.HasNCap 4 S) : C.Label S

The canonical labeling of a cap-4-free finset by Cap4FreeSlope.

Equations

• cap4FreeLabel h = { Slope := Cap4FreeSlope C S, extend_left := ⋯, extend_right := ⋯ }

theorem Config.Cup.extend_left {α : Type u_1} [LinearOrder α] {C : Config α} {S : Finset α} {label : C.Label S} {l : List α} (l_cup : C.Cup l) {a b : α} (s_ab : ¬label.Slope a b) (ha : a ∈ S) (hab : a < b) (l_in_S : l.In S) (b_head_l : b ∈ l.head?) : C.Cup (a :: l)

theorem Config.Cup.extend_right {α : Type u_1} [LinearOrder α] {C : Config α} {S : Finset α} {label : C.Label S} {l : List α} (l_cup : C.Cup l) {a b : α} (s_ab : label.Slope a b) (hab : a < b) (hb : b ∈ S) (l_in_S : l.In S) (a_last_l : a ∈ l.getLast?) : C.Cup (l ++ [b])

theorem Config.NCup.extend_left {α : Type u_1} [LinearOrder α] {C : Config α} {S : Finset α} {label : C.Label S} {n : ℕ} {l : List α} (l_ncup : C.NCup n l) {a b : α} (s_ab : ¬label.Slope a b) (ha : a ∈ S) (hab : a < b) (l_in_S : l.In S) (b_head_l : b ∈ l.head?) : C.NCup (n + 1) (a :: l)

theorem Config.NCup.extend_right {α : Type u_1} [LinearOrder α] {C : Config α} {S : Finset α} {label : C.Label S} {n : ℕ} {l : List α} (l_ncup : C.NCup n l) {a b : α} (s_ab : label.Slope a b) (hab : a < b) (hb : b ∈ S) (l_in_S : l.In S) (a_last_l : a ∈ l.getLast?) : C.NCup (n + 1) (l ++ [b])

def Config.Label.Mirror {α : Type u_1} [LinearOrder α] {C : Config α} {S : Finset α} (label : C.Label S) : C.Mirror.Label S.Mirror

The mirror labeling on the order dual, induced by negating the mirrored slope.

Equations

• label.Mirror = { Slope := fun (a b : αᵒᵈ) => ¬Mirror2 label.Slope a b, extend_left := ⋯, extend_right := ⋯ }

theorem Mirror_slope {α : Type u_1} [LinearOrder α] {C : Config α} {S : Finset α} {label : C.Label S} {a b : α} : ¬label.Mirror.Slope (OrderDual.toDual b) (OrderDual.toDual a) ↔ label.Slope a b