toOption — Mathlib

English

For any a ∈ Part α, b ∈ β, f : α → β, a.toOption.elim b f equals the case distinction: if a.Dom then f(a.get h) else b.

Русский

Для любого a ∈ Part α, b ∈ β, f : α → β, a.toOption.elim b f равняетсяразличие по случаю: если a.Dom, то f(a.get h), иначе b.

LaTeX

$$$ a.\\toOption.elim b f = \\text{if } h : a.\\Dom \\text{ then } f(a.\\get h) \\text{ else } b $$$

Lean4

protected theorem toOption {o : Part α} [Decidable o.Dom] (h : o.Dom) : o.toOption = o.get h :=
  dif_pos h

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