liftRel_pure_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem liftRel_pure_left (R : α → β → Prop) (a : α) (cb : Computation β) :
    LiftRel R (pure a) cb ↔ ∃ b, b ∈ cb ∧ R a b :=
  ⟨fun ⟨l, _⟩ => l (ret_mem _), fun ⟨b, mb, ab⟩ =>
    ⟨fun {a'} ma' => by rw [eq_of_pure_mem ma']; exact ⟨b, mb, ab⟩, fun {b'} mb' =>
      ⟨_, ret_mem _, by rw [mem_unique mb' mb]; exact ab⟩⟩⟩

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