terminates_map_iff — Mathlib

English

A stream terminates after finitely many steps if and only if its mapped stream terminates after the same number of steps.

Русский

Поток завершается в конечное время тогда и только тогда, когда отображенный поток завершается за те же шаги.

LaTeX

$$$(map f s).Terminates \Leftrightarrow s.Terminates$$$

Lean4

@[simp]
theorem terminates_map_iff {f : α → β} {s : Seq α} : (map f s).Terminates ↔ s.Terminates := by simp [Terminates]

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