rfind_min

Mathlib.Computability.Partrec

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

English

If n ∈ rfind p, then for every m < n, p(m) = false.

Русский

Если n ∈ rfind p, то для каждого m < n p(m) = false.

LaTeX

$$n ∈ rfind p → ∀ m < n, false ∈ p m$$

Lean4

theorem rfind_min {p : ℕ →. Bool} {n : ℕ} (h : n ∈ rfind p) : ∀ {m : ℕ}, m < n → false ∈ p m :=
  @(h.snd ▸ @((rfindX p h.fst).2.2))

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

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

Разделы

Аффилиация

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