Theorems · Theorem · logic and foundations

Computation.parallel_congr_left

∀ {α : Type u} {S T : Stream'.WSeq (Computation α)} {a : α},
  (∀ s ∈ S, s.Promises a) →
    Stream'.WSeq.LiftRel Computation.Equiv S T → (Computation.parallel S).Equiv (Computation.parallel T)

Defined in

Mathlib.Data.Seq.Parallel

Cited by

1 results in Mathlib

Foundations

Depth 43 from the axioms · uses propext, Classical.choice, Quot.sound