toOption_eq_none — Mathlib

English

The toOption of a Part is none exactly when the domain is false; equivalently, o.toOption = none ↔ ¬ o.Dom.

Русский

toOption части равна none тогда и только тогда, когда область определения ложна; то есть o.toOption = none ⇔ ¬ o.Dom.

LaTeX

$$$$o.toOption = \text{none} \;\iff\; \neg o.Dom.$$$$

Lean4

@[simp]
theorem toOption_eq_none (o : Part α) [Decidable o.Dom] : o.toOption = none ↔ ¬o.Dom := by
  by_cases h : o.Dom <;> simp [h, toOption]

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