English
The toOption of a bind equals the option-elimination of o composed with toOption and f.
Русский
toOption связывания равен разбору toOption по o и (f a).toOption.
LaTeX
$$$ (o.\bind f).toOption = o.toOption.elim \text{Option.none} (\lambda a, (f a).toOption) $$$
Lean4
theorem bind_toOption (f : α → Part β) (o : Part α) [Decidable o.Dom] [∀ a, Decidable (f a).Dom]
[Decidable (o.bind f).Dom] : (o.bind f).toOption = o.toOption.elim Option.none fun a => (f a).toOption :=
by
by_cases h : o.Dom
· simp_rw [h.toOption, h.bind]
rfl
· rw [Part.toOption_eq_none_iff.2 h]
exact Part.toOption_eq_none_iff.2 fun ho => h ho.of_bind
