Pairwise_tail — Mathlib

English

If a sequence s is Pairwise under R, then its tail s.tail is also Pairwise under R.

Русский

Если последовательность s попарно связана по R, то её хвост также попарно связан по R.

LaTeX

$$$\\text{Pairwise}(R, s) \\Rightarrow \\text{Pairwise}(R, s.tail)$$$

Lean4

theorem Pairwise_tail {R : α → α → Prop} {s : Seq α} (h : s.Pairwise R) : s.tail.Pairwise R :=
  by
  cases s
  · simp
  · simp [h.cons_elim.right]

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