liftRel_think_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem liftRel_think_right (R : α → β → Prop) (ca : Computation α) (cb : Computation β) :
    LiftRel R ca (think cb) ↔ LiftRel R ca cb := by rw [← LiftRel.swap R, ← LiftRel.swap R]; apply liftRel_think_left

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