LeanPool.ErdosTuzaValtr.Config.Lemmas #

Imported Lean Pool material for LeanPool.ErdosTuzaValtr.Config.Lemmas.

source

@[simp]

theorem Config.Cap.nil {α : Type u_1} [LinearOrder α] {C : Config α} :

C.Cap []

source

@[simp]

theorem Config.Cap.singleton {α : Type u_1} [LinearOrder α] {C : Config α} (a : α) :

C.Cap [a]

source

@[simp]

theorem Config.Cap.pair {α : Type u_1} [LinearOrder α] {C : Config α} {a b : α} :

C.Cap [a, b] ↔ a < b

source

@[simp]

theorem Config.Cap.cons3 {α : Type u_1} [LinearOrder α] {C : Config α} {a b c : α} {l : List α} :

C.Cap (a :: b :: c :: l) ↔ a < b ∧ C.Cap3 a b c ∧ C.Cap (b :: c :: l)

source

@[simp]

theorem Config.Cap.append_cons3 {α : Type u_1} [LinearOrder α] {C : Config α} {a b c : α} {l1 l2 : List α} :

C.Cap (l1 ++ a :: b :: c :: l2) ↔ C.Cap (l1 ++ [a, b]) ∧ C.Cap3 a b c ∧ C.Cap (b :: c :: l2)

source

theorem Config.Cap.dropLast {α : Type u_1} [LinearOrder α] {C : Config α} {l : List α} (h : C.Cap l) :

C.Cap l.dropLast

source

theorem Config.Cap.tail {α : Type u_1} [LinearOrder α] {C : Config α} {l : List α} (h : C.Cap l) :

C.Cap l.tail

source

theorem Config.NCap.dropLast {α : Type u_1} [LinearOrder α] {C : Config α} {n : ℕ} {l : List α} (h : C.NCap (n + 1) l) :

C.NCap n l.dropLast

source

theorem Config.NCap.tail {α : Type u_1} [LinearOrder α] {C : Config α} {n : ℕ} {l : List α} (h : C.NCap (n + 1) l) :

C.NCap n l.tail

source

@[simp]

theorem Config.Cup.nil {α : Type u_1} [LinearOrder α] {C : Config α} :

C.Cup []

source

@[simp]

theorem Config.Cup.singleton {α : Type u_1} [LinearOrder α] {C : Config α} (a : α) :

C.Cup [a]

source

@[simp]

theorem Config.Cup.pair {α : Type u_1} [LinearOrder α] {C : Config α} {a b : α} :

C.Cup [a, b] ↔ a < b

source

@[simp]

theorem Config.Cup.cons3 {α : Type u_1} [LinearOrder α] {C : Config α} {a b c : α} {l : List α} :

C.Cup (a :: b :: c :: l) ↔ a < b ∧ C.Cup3 a b c ∧ C.Cup (b :: c :: l)

source

@[simp]

theorem Config.Cup.append_cons3 {α : Type u_1} [LinearOrder α] {C : Config α} {a b c : α} {l1 l2 : List α} :

C.Cup (l1 ++ a :: b :: c :: l2) ↔ C.Cup (l1 ++ [a, b]) ∧ C.Cup3 a b c ∧ C.Cup (b :: c :: l2)

source

theorem Config.Cup.dropLast {α : Type u_1} [LinearOrder α] {C : Config α} {l : List α} (h : C.Cup l) :

C.Cup l.dropLast

source

theorem Config.Cup.take {α : Type u_1} [LinearOrder α] {C : Config α} {l : List α} (h : C.Cup l) (n : ℕ) :

C.Cup (List.take n l)

source

theorem Config.Cup.drop {α : Type u_1} [LinearOrder α] {C : Config α} {l : List α} (h : C.Cup l) (n : ℕ) :

C.Cup (List.drop n l)

source

theorem Config.Cup.tail {α : Type u_1} [LinearOrder α] {C : Config α} {l : List α} (h : C.Cup l) :

C.Cup l.tail

source

theorem Config.Cup.head_lt_getLast {α : Type u_1} [LinearOrder α] {C : Config α} {l : List α} (l_cup : C.Cup l) (p q : α) (hl : 2 ≤ l.length) (hp : p ∈ l.head?) (hq : q ∈ l.getLast?) :

p < q

source

theorem Config.Cup.head?_lt_getLast? {α : Type u_1} [LinearOrder α] {C : Config α} {l : List α} (l_cup : C.Cup l) (p q : α) (hl : 2 ≤ l.length) (hp : p ∈ l.head?) (hq : q ∈ l.getLast?) :

p < q

Compatibility alias for the upstream theorem name.

source

@[simp]

theorem Config.NCup.nil {α : Type u_1} [LinearOrder α] {C : Config α} :

C.NCup 0 []

source

@[simp]

theorem Config.NCup.singleton {α : Type u_1} [LinearOrder α] {C : Config α} (a : α) :

C.NCup 1 [a]

source

@[simp]

theorem Config.NCup.pair {α : Type u_1} [LinearOrder α] {C : Config α} {a b : α} :

C.NCup 2 [a, b] ↔ a < b

source

@[simp]

theorem Config.NCup.cons3 {α : Type u_1} [LinearOrder α] {C : Config α} {n : ℕ} {a b c : α} {l : List α} :

C.NCup (n + 1) (a :: b :: c :: l) ↔ a < b ∧ C.Cup3 a b c ∧ C.NCup n (b :: c :: l)

source

theorem Config.NCup.dropLast {α : Type u_1} [LinearOrder α] {C : Config α} {n : ℕ} {l : List α} (h : C.NCup (n + 1) l) :

C.NCup n l.dropLast

source

theorem Config.NCup.dropLast_append_last {α : Type u_1} [LinearOrder α] {C : Config α} {n : ℕ} {l : List α} (h : C.NCup (n + 1) l) :

∃ (l' : List α) (a : α), l = l' ++ [a] ∧ C.NCup n l'

source

theorem Config.NCup.tail {α : Type u_1} [LinearOrder α] {C : Config α} {n : ℕ} {l : List α} (h : C.NCup (n + 1) l) :

C.NCup n l.tail

source

theorem Config.NCup.cons_head_tail {α : Type u_1} [LinearOrder α] {C : Config α} {n : ℕ} {l : List α} (h : C.NCup (n + 1) l) :

∃ (a : α) (l' : List α), l = a :: l' ∧ C.NCup n l'

source

theorem Config.NCup.take_head_last {α : Type u_1} [LinearOrder α] {C : Config α} {n : ℕ} {l : List α} (h : C.NCup (n + 2) l) :

∃ (a : α) (l' : List α) (b : α), l = a :: l' ++ [b] ∧ C.NCup n l'

source

theorem Config.NCup.take_left_with_head {α : Type u_1} [LinearOrder α] {C : Config α} {n : ℕ} {l : List α} (h : C.NCup n l) (m : ℕ) (p : α) :

1 ≤ m → m ≤ n → p ∈ l.head? → ∃ l' ⊆ l, C.NCup m l' ∧ p ∈ l'.head?

source

theorem Config.NCup.take_right_with_last {α : Type u_1} [LinearOrder α] {C : Config α} {n : ℕ} {l : List α} (h : C.NCup n l) (m : ℕ) (p : α) :

1 ≤ m → m ≤ n → p ∈ l.getLast? → ∃ l' ⊆ l, C.NCup m l' ∧ p ∈ l'.getLast?

source

theorem Config.NCup.head_lt_getLast {α : Type u_1} [LinearOrder α] {C : Config α} {n : ℕ} {l : List α} (l_ncup : C.NCup (n + 2) l) (p q : α) (hp : p ∈ l.head?) (hq : q ∈ l.getLast?) :

p < q

source

theorem Config.NCup.head?_lt_getLast? {α : Type u_1} [LinearOrder α] {C : Config α} {n : ℕ} {l : List α} (l_ncup : C.NCup (n + 2) l) (p q : α) (hp : p ∈ l.head?) (hq : q ∈ l.getLast?) :

p < q

Compatibility alias for the upstream theorem name.

source

theorem Config.NCup.head_le_getLast {α : Type u_1} [LinearOrder α] {C : Config α} {n : ℕ} {l : List α} (l_ncup : C.NCup n l) (p q : α) (hp : p ∈ l.head?) (hq : q ∈ l.getLast?) :

p ≤ q

source

theorem Config.NCup.head?_le_getLast? {α : Type u_1} [LinearOrder α] {C : Config α} {n : ℕ} {l : List α} (l_ncup : C.NCup n l) (p q : α) (hp : p ∈ l.head?) (hq : q ∈ l.getLast?) :

p ≤ q

Compatibility alias for the upstream theorem name.

source

theorem ncup_is_ngon {α : Type u_1} [LinearOrder α] {C : Config α} {n : ℕ} {S : Finset α} (hn : 2 ≤ n) (h : C.HasNCup n S) :

C.HasNGon n S

source

theorem hasNCap_supset {α : Type u_1} [LinearOrder α] {C : Config α} {n : ℕ} {S1 S2 : Finset α} (h : S1 ⊆ S2) (h1 : C.HasNCap n S1) :

C.HasNCap n S2

source

theorem hasNCup_supset {α : Type u_1} [LinearOrder α] {C : Config α} {n : ℕ} {S1 S2 : Finset α} (h : S1 ⊆ S2) (h1 : C.HasNCup n S1) :

C.HasNCup n S2

source

theorem hasNGon_supset {α : Type u_1} [LinearOrder α] {C : Config α} {n : ℕ} {S1 S2 : Finset α} (h : S1 ⊆ S2) (h1 : C.HasNGon n S1) :

C.HasNGon n S2

source

theorem hasNCup_le {α : Type u_1} [LinearOrder α] {C : Config α} {n m : ℕ} {S : Finset α} (h : n ≤ m) :

C.HasNCup m S → C.HasNCup n S