rfind_spec

Mathlib.Computability.Partrec

URI: https://scilib.ai/kg/mathlib#Nat.rfind_spec

English

If n is in the domain of rfind p, then p(n) = true.

Русский

Если n принадлежит области определения rfind p, то p(n) равно true.

LaTeX

$$n ∈ rfind p → true ∈ p n$$

Lean4

theorem rfind_spec {p : ℕ →. Bool} {n : ℕ} (h : n ∈ rfind p) : true ∈ p n :=
  h.snd ▸ (rfindX p h.fst).2.1

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru