isChain_iff_forall_rel_of_append_cons_cons

English

IsChain R l is equivalent to the property that for all a,b and l1,l2 with l = l1 ++ a :: b :: l2, we have R a b.

Русский

IsChain R l эквивалентно тому, что для всех a,b и разделов l1,l2 с l = l1 ++ a :: b :: l2 выполняется R a b.

LaTeX

$$$IsChain\\;R\\;l \\iff ∀\\{a,b\\}, \\{l_1,l_2\\}, l = l_1 ++ a :: b :: l_2 \\rightarrow R\\;a\\;b$$$

Lean4

theorem isChain_iff_forall_rel_of_append_cons_cons {l : List α} :
    IsChain R l ↔ ∀ ⦃a b l₁ l₂⦄, l = l₁ ++ a :: b :: l₂ → R a b :=
  by
  refine ⟨fun h _ _ _ _ eq => (isChain_append_cons_cons.mp (eq ▸ h)).2.1, ?_⟩
  induction l using twoStepInduction with
  | nil
  | singleton => grind
  | cons_cons head head' tail _
    ih =>
    refine fun h ↦ isChain_cons_cons.mpr ⟨h (nil_append _).symm, ih _ fun ⦃a b l₁ l₂⦄ eq => ?_⟩
    apply h
    rw [eq, cons_append]

Похожие утверждения