imp_of_mem_tail_imp — Mathlib

English

If H ensures S on tail transitions from any a to b along a chain, then IsChain S l holds whenever IsChain R l holds.

Русский

Если H задаёт переходы хвоста, то IsChain S сохраняется по отношению к IsChain R.

LaTeX

$$$ \\forall S, (\\forall a,b, a \\in l \\rightarrow b \\in l.tail \\rightarrow R\\,a\\,b \\rightarrow S\\,a\\,b) \\rightarrow IsChain\\;R\\;l \\rightarrow IsChain\\;S\\;l$$$

Lean4

theorem imp_of_mem_tail_imp {S : α → α → Prop} {l : List α} (H : ∀ a b : α, a ∈ l → b ∈ l.tail → R a b → S a b)
    (p : IsChain R l) : IsChain S l := by induction p with grind

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