terminates_cons_iff — Mathlib

English

(cons x s) terminates iff s terminates.

Русский

(cons x s) завершается тогда и только тогда, когда s завершается.

LaTeX

$$$ (\\mathrm{cons}\\ x\\ s).Terminates \\iff s.Terminates $$$

Lean4

@[simp]
theorem terminates_cons_iff {x : α} {s : Seq α} : (cons x s).Terminates ↔ s.Terminates :=
  by
  constructor <;> intro ⟨n, h⟩
  · exact ⟨n, cons_terminatedAt_succ_iff.mp (terminated_stable _ (Nat.le_succ _) h)⟩
  · exact ⟨n + 1, cons_terminatedAt_succ_iff.mpr h⟩

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