Theorems · Theorem · logic and foundations

Part.bind_assoc

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_4} (f : Part α) (g : α → Part β) (k : β → Part γ),
  (f.bind g).bind k = f.bind fun x => (g x).bind k

Defined in

Mathlib.Data.Part

Cited by

5 results in Mathlib

Foundations

Depth 13 from the axioms · uses propext, Quot.sound