LeanPool.ErdosTuzaValtr.Lib.List.Chain3

Imported Lean Pool material for LeanPool.ErdosTuzaValtr.Lib.List.Chain3.

theorem List.chain3_split {α : Type u_1} {R : α → α → α → Prop} {a b c d : α} {l1 l2 : List α} : Chain3 R a b (l1 ++ c :: d :: l2) ↔ Chain3 R a b (l1 ++ [c, d]) ∧ Chain3 R c d l2

@[simp]

theorem List.chain3_append_cons3 {α : Type u_1} {R : α → α → α → Prop} {a b c d e : α} {l1 l2 : List α} : Chain3 R a b (l1 ++ c :: d :: e :: l2) ↔ Chain3 R a b (l1 ++ [c, d]) ∧ R c d e ∧ Chain3 R d e l2

@[simp]

theorem List.chain3'_nil {α : Type u_1} {R : α → α → α → Prop} : Chain3' R []

@[simp]

theorem List.chain3'_singleton {α : Type u_1} {R : α → α → α → Prop} (a : α) : Chain3' R [a]

@[simp]

theorem List.chain3'_pair {α : Type u_1} {R : α → α → α → Prop} (a b : α) : Chain3' R [a, b]

@[simp]

theorem List.chain3'_cons {α : Type u_1} {R : α → α → α → Prop} {x y z : α} {l : List α} : Chain3' R (x :: y :: z :: l) ↔ R x y z ∧ Chain3' R (y :: z :: l)

theorem List.chain3'_split {α : Type u_1} {R : α → α → α → Prop} {a b : α} {l1 l2 : List α} : Chain3' R (l1 ++ a :: b :: l2) ↔ Chain3' R (l1 ++ [a, b]) ∧ Chain3' R (a :: b :: l2)

@[simp]

theorem List.chain3'_append_cons3 {α : Type u_1} {R : α → α → α → Prop} {a b c : α} {l1 l2 : List α} : Chain3' R (l1 ++ a :: b :: c :: l2) ↔ Chain3' R (l1 ++ [a, b]) ∧ R a b c ∧ Chain3' R (b :: c :: l2)

theorem List.Chain3'.left_of_append {α : Type u_1} {R : α → α → α → Prop} {l1 l2 : List α} (h : Chain3' R (l1 ++ l2)) : Chain3' R l1

theorem List.Chain3'.right_of_append {α : Type u_1} {R : α → α → α → Prop} {l1 l2 : List α} (h : Chain3' R (l1 ++ l2)) : Chain3' R l2

theorem List.Chain3'.infix {α : Type u_1} {R : α → α → α → Prop} {l₁ l : List α} (h : Chain3' R l) (h' : l₁ <:+: l) : Chain3' R l₁

theorem List.Chain3'.suffix {α : Type u_1} {R : α → α → α → Prop} {l₁ l : List α} (h : Chain3' R l) (h' : l₁ <:+ l) : Chain3' R l₁

theorem List.Chain3'.prefix {α : Type u_1} {R : α → α → α → Prop} {l₁ l : List α} (h : Chain3' R l) (h' : l₁ <+: l) : Chain3' R l₁

theorem List.Chain3'.drop {α : Type u_1} {R : α → α → α → Prop} {l : List α} (h : Chain3' R l) (n : ℕ) : Chain3' R (List.drop n l)

theorem List.Chain3'.dropLast {α : Type u_1} {R : α → α → α → Prop} {l : List α} (h : Chain3' R l) : Chain3' R l.dropLast

theorem List.Chain3'.take {α : Type u_1} {R : α → α → α → Prop} {l : List α} (h : Chain3' R l) (n : ℕ) : Chain3' R (List.take n l)

theorem List.Chain3'.tail {α : Type u_1} {R : α → α → α → Prop} {l : List α} (h : Chain3' R l) : Chain3' R l.tail

theorem List.chain3'_mirror {α : Type u_1} {R : α → α → α → Prop} [LinearOrder α] {l : List α} : Chain3' (Mirror3 R) l.Mirror ↔ Chain3' R l