terminates_map_iff — Mathlib

English

The termination of map f s is equivalent to the termination of s: Terminates (map f s) ↔ Terminates s.

Русский

Завершение отображения map f s эквивалентно завершению s: Terminates (map f s) ⇔ Terminates s.

LaTeX

$$$\operatorname{Terminates}\big(\operatorname{map} f\, s\big) \iff \operatorname{Terminates}(s)$$$

Lean4

theorem terminates_map_iff (f : α → β) (s : Computation α) : Terminates (map f s) ↔ Terminates s :=
  ⟨fun ⟨⟨_, h⟩⟩ =>
    let ⟨_, h1, _⟩ := exists_of_mem_map h
    ⟨⟨_, h1⟩⟩,
    @Computation.terminates_map _ _ _ _⟩
    -- Parallel computation

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