isChain_attach — Mathlib

English

Induction along a concatenation l ++ [b] propagates a property p along the whole concatenated list from its head to the end.

Русский

Индукция по конкатенации l ++ [b] распространяет свойство p по всей цепи от головы до конца.

LaTeX

$$$IsChain\\, R\\, (l ++ [b]) \\rightarrow \\big( Eq (head (l ++ [b])) a \\big) \\rightarrow \\Big( \\forall x \\in l ++ [b], p x \\Big)$$$

Lean4

theorem isChain_attach {l : List α} {r : { a // a ∈ l } → { a // a ∈ l } → Prop} :
    l.attach.IsChain r ↔ l.IsChain fun a b ↦ ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩ :=
  isChain_attachWith fun _ ↦ id

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