English
In a linear order, if the head-to-tail chain holds for a :: as and m is a chain, and m ≤ as in the order, then a :: m is a chain.
Русский
При линейном порядке, если цепь для a :: as верна и m образует цепь, и m ≤ as, тогда a :: m образует цепь.
LaTeX
$$$\\forall {\\alpha}, [\\text{LinearOrder}\\, \\alpha], \\forall a, as, m:\\, \\text{List }\\alpha, IsChain(GT) (a :: as) \\rightarrow IsChain(GT) m \\\\rightarrow m \\le as \\rightarrow IsChain(GT) (a :: m)$$$
Lean4
/-- Given a chain `l`, such that a predicate `p` holds for its head if it is nonempty,
and if `r x y → p x → p y`, then the predicate is true everywhere in the chain.
That is, we can propagate the predicate down the chain.
-/
theorem induction (p : α → Prop) (l : List α) (h : IsChain r l) (carries : ∀ ⦃x y : α⦄, r x y → p x → p y)
(initial : (lne : l ≠ []) → p (l.head lne)) : ∀ i ∈ l, p i := by
induction l using twoStepInduction with
| nil => grind [not_mem_nil]
| singleton => grind
| cons_cons a b l IH IH2 => grind
