mem_parallel — Mathlib

English

If every s ∈ S promises a, then for any c ∈ S and a ∈ c, we have a ∈ parallel S.

Русский

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

LaTeX

$$$ \forall a, \forall c \in S, a \in c \Rightarrow a \in \mathrm{parallel}(S).$$$

Lean4

theorem mem_parallel {S : WSeq (Computation α)} {a} (H : ∀ s ∈ S, s ~> a) {c} (cs : c ∈ S) (ac : a ∈ c) :
    a ∈ parallel S := by
  haveI := terminates_of_mem ac
  haveI := terminates_parallel cs
  exact mem_of_promises _ (parallel_promises H)

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