Theorems · Theorem · logic and foundations

Computation.liftRel_map

∀ {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} (R : α → β → Prop) (S : γ → δ → Prop) {s1 : Computation α}
  {s2 : Computation β} {f1 : α → γ} {f2 : β → δ},
  Computation.LiftRel R s1 s2 →
    (∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)) → Computation.LiftRel S (Computation.map f1 s1) (Computation.map f2 s2)

Defined in

Mathlib.Data.Seq.Computation

Cited by

2 results in Mathlib

Foundations

Depth 38 from the axioms · uses propext, Quot.sound