rfind — Mathlib

English

The rfind function is defined as a partial function that maps a predicate p to the least n with p(n) = true, when such n exists by the given conditions.

Русский

Функция rfind определяется как частичная функция, сопоставляющая предикату p наименьшее n, для которого p(n) истинно, при условии существования такового n.

LaTeX

$$rfind (p) : Part ℕ := ⟨_, fun h => (rfindX p h).1⟩$$

Lean4

/-- Find the smallest `n` satisfying `p n`, where all `p k` for `k < n` are defined as false.
Returns a `Part`. -/
def rfind (p : ℕ →. Bool) : Part ℕ :=
  ⟨_, fun h => (rfindX p h).1⟩

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