liftRel_think_left — Mathlib

English

Applying think to the left component preserves LiftRel: LiftRel R (think ca) cb is equivalent to LiftRel R ca cb.

Русский

Применение think к левой части сохраняет LiftRel: LiftRel R (think ca) cb эквивалентно LiftRel R ca cb.

LaTeX

$$$\\mathrm{LiftRel}\\,R\\,(\\mathrm{think}\\ ca)\\ cb \\ \\leftrightarrow\\ \\mathrm{LiftRel}\\,R\\ ca\\ cb$$

Lean4

@[simp]
theorem liftRel_think_left (R : α → β → Prop) (ca : Computation α) (cb : Computation β) :
    LiftRel R (think ca) cb ↔ LiftRel R ca cb :=
  and_congr (forall_congr' fun _ => imp_congr ⟨of_think_mem, think_mem⟩ Iff.rfl)
    (forall_congr' fun _ => imp_congr Iff.rfl <| exists_congr fun _ => and_congr ⟨of_think_mem, think_mem⟩ Iff.rfl)

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