evalOpt — Mathlib

English

EvalOpt maps a partial function to an Option value by returning Some(y) when x ∈ Dom f and f(x) contains y, otherwise None.

Русский

EvalOpt переводит частичную функцию в значение типа Option: возвращает Some(y) тогда, когда x принадлежит области определения и y ∈ f(x); иначе None.

LaTeX

$$$\\mathrm{evalOpt}(f)(x) = \\mathrm{Part.toOption}(D\\,x)$$$

Lean4

/-- Evaluate a partial function to return an `Option` -/
def evalOpt (f : α →. β) [D : DecidablePred (· ∈ Dom f)] (x : α) : Option β :=
  @Part.toOption _ _ (D x)

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