toOption_isSome — Mathlib

English

For any partial value o, the toOption value is Some exactly when the domain exists; i.e., o.toOption.isSome holds if and only if o.Dom.

Русский

Для любого частичного значения o такая же величина toOption равна Some тогда и только тогда, когда существует область определения o.Dom.

LaTeX

$$$$\forall o:\mathrm{Part}\,\alpha\,\big[\mathsf{Decidable}\,o.Dom\big],\; o.toOption.isSome \;\iff\; o.Dom.$$$$

Lean4

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

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