concat_induction_head — Mathlib

English

Aelaborated induction principle extracting the head b from a :: l based on concat_induction.

Русский

Уточненная индукция, получаемая из concat_induction на голове b.

LaTeX

$$$IsChain\\, R\\, (l ++ [b]) \\Rightarrow Eq (head (l ++ [b])) a \\Rightarrow \\forall p, ... \\Rightarrow p b$$$

Lean4

@[elab_as_elim]
theorem concat_induction_head (p : α → Prop) (l : List α) (h : IsChain r (l ++ [b]))
    (hb : head (l ++ [b]) (concat_ne_nil _ _) = a) (carries : ∀ ⦃x y : α⦄, r x y → p x → p y) (initial : p a) : p b :=
  (IsChain.concat_induction p l h hb carries initial) _ mem_concat_self

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