bind_promises — Mathlib

English

If s promises to a and f a promises to b, then bind s f promises to b.

Русский

Если s обещает a и f a обещает b, тогда bind s f обещает b.

LaTeX

$$$$ (s \xrightarrow{\text{promises}} a) \wedge (f a \xrightarrow{\text{promises}} b) \Rightarrow (\operatorname{bind} s f) \xrightarrow{\text{promises}} b. $$$$

Lean4

theorem bind_promises {s : Computation α} {f : α → Computation β} {a b} (h1 : s ~> a) (h2 : f a ~> b) : bind s f ~> b :=
  fun b' bB => by
  rcases exists_of_mem_bind bB with ⟨a', a's, ba'⟩
  rw [← h1 a's] at ba'; exact h2 ba'

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