cons_terminatedAt_succ_iff — Mathlib

English

For any x and s, (cons x s).TerminatedAt(n+1) holds iff s.TerminatedAt(n).

Русский

Для любых x и s, (cons x s).TerminatedAt(n+1) истинно тогда и только тогда, когда s.TerminatedAt(n).

LaTeX

$$$\\text{TerminatedAt}(\\mathrm{cons}\\ x\\ s, n+1) \\iff \\text{TerminatedAt}(s, n)$$$

Lean4

@[simp]
theorem cons_terminatedAt_succ_iff {x : α} {s : Seq α} {n : ℕ} : (cons x s).TerminatedAt (n + 1) ↔ s.TerminatedAt n :=
  by simp [TerminatedAt]

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