toOption_eq_none_iff — Mathlib

English

For any Part α and a choice of decidable dom, a.toOption equals None if and only if its domain is empty.

Русский

Для любого Part α и выбора decidable dom выполняется a.toOption = None тогда и только тогда, когда область определения пустая.

LaTeX

$$$a.{\\rm toOption} = \\text{Option.none} \\iff \\neg a.Dom$$$

Lean4

theorem toOption_eq_none_iff {a : Part α} [Decidable a.Dom] : a.toOption = Option.none ↔ ¬a.Dom :=
  Ne.dite_eq_right_iff fun _ => Option.some_ne_none _

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