bind — Mathlib

English

If o is defined (h : o.Dom) and f : α → Part β, then o.bind f = f (o.get h).

Русский

Если o определено (h : o.Dom) и f : α → Part β, тогда o.bind f = f(o.get h).

LaTeX

$$$ \forall {o} {f} (h : o.\\Dom), o.\\bind f = f(o.\\get h)$$$

Lean4

protected theorem bind {o : Part α} (h : o.Dom) (f : α → Part β) : o.bind f = f (o.get h) :=
  by
  ext b
  simp only [Part.mem_bind_iff]
  refine ⟨?_, fun hb => ⟨o.get h, Part.get_mem _, hb⟩⟩
  rintro ⟨a, ha, hb⟩
  rwa [Part.get_eq_of_mem ha]

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