bind_eq_some' — Mathlib

English

A bind of x with f equals some b iff there exists a with x = some a and f a = some b.

Русский

Связывание x с f равно some b тогда и только тогда, когда существует a such that x = some a и f a = some b.

LaTeX

$$$$ x\bind f = \mathrm{some} b \iff \exists a, x = \mathrm{some} a \land f a = \mathrm{some} b. $$$$

Lean4

@[deprecated bind_eq_some_iff (since := "2025-04-10")]
theorem bind_eq_some' {x : Option α} {f : α → Option β} {b : β} : x.bind f = some b ↔ ∃ a, x = some a ∧ f a = some b :=
  bind_eq_some_iff

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