exists_of_mem_bind — Mathlib

English

From b ∈ bind s f, there exists a ∈ s with b ∈ f a.

Русский

Из b ∈ bind s f следует, что существует a ∈ s такой, что b ∈ f a.

LaTeX

$$$$ b \in \operatorname{bind} s f \Rightarrow \exists a \in s,\ b \in f(a). $$$$

Lean4

theorem exists_of_mem_bind {s : Computation α} {f : α → Computation β} {b} (h : b ∈ bind s f) : ∃ a ∈ s, b ∈ f a :=
  let ⟨_, h⟩ := exists_results_of_mem h
  let ⟨a, _, _, h1, h2, _⟩ := of_results_bind h
  ⟨a, h1.mem, h2.mem⟩

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