bind_assoc — Mathlib

English

Binding is associative: (f.bind g).bind k = f.bind (λ x, (g x).bind k).

Русский

Связывание по монадной операции ассоциативно: (f.bind g).bind k = f.bind(λ x, (g x).bind k).

LaTeX

$$$ (f.\bind g).\bind k = f.\bind (\\lambda x, (g x).\bind k) $$$

Lean4

theorem bind_assoc {γ} (f : Part α) (g : α → Part β) (k : β → Part γ) :
    (f.bind g).bind k = f.bind fun x => (g x).bind k :=
  ext fun a => by
    simp only [mem_bind_iff]
    exact ⟨fun ⟨_, ⟨_, h₁, h₂⟩, h₃⟩ => ⟨_, h₁, _, h₂, h₃⟩, fun ⟨_, h₁, _, h₂, h₃⟩ => ⟨_, ⟨_, h₁, h₂⟩, h₃⟩⟩

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