pbind_eq_none — Mathlib

English

Under a certain hypothesis, x.pbind f equals none iff x equals none.

Русский

При некотором предположении, x.pbind f = none тогда и только тогда, когда x = none.

LaTeX

$$$$ (\forall a (H : a \in x), f a H = \mathrm{none} \Rightarrow x = \mathrm{none}) \Rightarrow (x.\mathrm{pbind} f = \mathrm{none} \iff x = \mathrm{none}). $$$$

Lean4

theorem pbind_eq_none {f : ∀ a : α, a ∈ x → Option β} (h' : ∀ a (H : a ∈ x), f a H = none → x = none) :
    x.pbind f = none ↔ x = none := by grind [cases Option]

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