terminates_map — Mathlib

English

If a computation s terminates, then map f s terminates.

Русский

Если вычисление s завершается, то вычисление map f s завершается.

LaTeX

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

Lean4

instance terminates_map (f : α → β) (s : Computation α) [Terminates s] : Terminates (map f s) := by rw [← bind_pure];
  exact terminates_of_mem (mem_bind (get_mem s) (get_mem (α := β) (f (get s))))

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