parallel_congr_right — Mathlib

English

If every t ∈ T promises a and S is lift-relatable to T, then (parallel S) is equivalent to (parallel T).

Русский

Если для всех t ∈ T обещано a и S сопоставимо по LiftRel с T, то parallel S эквивалентен parallel T.

LaTeX

$$$ \forall S,T, a: \alpha, (\forall t \in T, t.Promises a) \rightarrow (S \LiftRel Equiv T) \Rightarrow (\mathrm{parallel}(S)) \Equiv (\mathrm{parallel}(T)).$$$

Lean4

theorem parallel_congr_right {S T : WSeq (Computation α)} {a} (h2 : ∀ t ∈ T, t ~> a) (H : S.LiftRel Equiv T) :
    parallel S ~ parallel T :=
  parallel_congr_left ((parallel_congr_lem H).2 h2) H

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