rfindOpt — Mathlib

English

Define rfindOpt f as the smallest n with f(n) defined, provided earlier values are undefined.

Русский

Определим rfindOpt f как минимальный n, для которого f(n) определено, при условии, что ранее значения не определены.

LaTeX

$$$\mathrm{rfindOpt}\{\alpha\}(f) = \mathrm{Option}.bind\bigl(\mathrm{rfind}(n \mapsto (f(n)).\mathrm{isSome})\bigr)\bigl( n \mapsto f(n) \bigr).$$$

Lean4

/-- Find the smallest `n` satisfying `f n`, where all `f k` for `k < n` are defined as false.
Returns a `Part`. -/
def rfindOpt {α} (f : ℕ → Option α) : Part α :=
  (rfind fun n => (f n).isSome).bind fun n => f n

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