liftRel_pure_right — Mathlib

English

LiftRel R ca (pure b) is equivalent to the existence of an a in ca with R a b.

Русский

LiftRel R ca (pure b) эквивалентно существованию a в ca такого, что R a b.

LaTeX

$$$\\mathrm{LiftRel}\\,R(ca)(\\mathrm{pure}\\ b) \\ \\leftrightarrow\\ \\exists a\\in ca\\, R\\ a\\ b$$$

Lean4

@[simp]
theorem liftRel_pure_right (R : α → β → Prop) (ca : Computation α) (b : β) :
    LiftRel R ca (pure b) ↔ ∃ a, a ∈ ca ∧ R a b := by rw [LiftRel.swap, liftRel_pure_left]

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