backwards_cons_induction — Mathlib

English

Starting from a chain a :: l ending at b, with head fixed by hb, the predicate propagates backwards from b to all elements of a :: l.

Русский

Из цепи a :: l с головой a, ограниченной hb, предикат распространяется обратно по всей цепи.

LaTeX

$$$IsChain\\, R\\, (a :: l) \\rightarrow Eq ((a::l).getLast ...) b \\rightarrow (\\forall x, R x y \\Rightarrow p y \\Rightarrow p x) \\Rightarrow p b \\Rightarrow \\forall i \\in a::l, p i$$$

Lean4

theorem backwards_cons_induction (p : α → Prop) (l : List α) (h : IsChain r (a :: l))
    (hb : getLast (a :: l) (cons_ne_nil _ _) = b) (carries : ∀ ⦃x y : α⦄, r x y → p y → p x) (final : p b) :
    ∀ i ∈ a :: l, p i :=
  h.backwards_induction _ _ carries (fun _ => hb ▸ final)

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