parallel_promises — Mathlib

English

If every s in S promises a value a, then the parallel composition parallel S promises a.

Русский

Если каждый элемент в S обещает значение a, то параллельная композиция parallel S обещает значение a.

LaTeX

$$$ \forall a,\ S:\mathrm{WSeq}(\mathrm{Computation}(\alpha)),\ (\forall s, s\in S \Rightarrow s\Promises a) \Rightarrow (\mathrm{parallel}\ S).Promises a$$$

Lean4

theorem parallel_promises {S : WSeq (Computation α)} {a} (H : ∀ s ∈ S, s ~> a) : parallel S ~> a := fun _ ma' =>
  let ⟨_, cs, ac⟩ := exists_of_mem_parallel ma'
  H _ cs ac

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