rfindOpt_spec

Mathlib.Computability.Partrec

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

English

If a is in rfindOpt f, then there exists n with a in f(n).

Русский

Если a принадлежит rfindOpt f, то существует n such that a ∈ f(n).

LaTeX

$$$a \in \mathrm{rfindOpt}(f) \Rightarrow \exists n, a \in f(n).$$$

Lean4

theorem rfindOpt_spec {α} {f : ℕ → Option α} {a} (h : a ∈ rfindOpt f) : ∃ n, a ∈ f n :=
  let ⟨n, _, h₂⟩ := mem_bind_iff.1 h
  ⟨n, mem_coe.1 h₂⟩

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

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

Разделы

Аффилиация

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