results_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 results_bind {s : Computation α} {f : α → Computation β} {a b m n} (h1 : Results s a m)
    (h2 : Results (f a) b n) : Results (bind s f) b (n + m) :=
  by
  have := h1.mem; revert m
  apply memRecOn this _ fun s IH => _
  · intro _ h1
    rw [ret_bind]
    rw [h1.len_unique (results_pure _)]
    exact h2
  · intro _ h3 _ h1
    rw [think_bind]
    obtain ⟨m', h⟩ := of_results_think h1
    obtain ⟨h1, e⟩ := h
    rw [e]
    exact results_think (h3 h1)

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