Pairwise_drop — Mathlib

English

If s is Pairwise under R, then for every n, the dropped sequence s.drop n is also Pairwise under R.

Русский

Если последовательность s попарно связана по R, то и последовательность, полученная удалением первых n элементов, тоже попарно связана по R.

LaTeX

$$$\\text{Pairwise}(R, s) \\Rightarrow \\forall n, \\; \\text{Pairwise}(R, s.drop n)$$$

Lean4

theorem Pairwise_drop {R : α → α → Prop} {s : Seq α} (h : s.Pairwise R) {n : ℕ} : (s.drop n).Pairwise R := by
  induction n with
  | zero => simpa
  | succ m ih => simp [drop, Pairwise_tail ih]

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