English
The domain of rfindOpt f is equivalent to the existence of some index n with a in f(n).
Русский
Область определения rfindOpt f эквивалентна существованию некоторого индекса n с a ∈ f(n).
LaTeX
$$$(\mathrm{rfindOpt}(f)).\mathrm{Dom} \;\leftrightarrow\; \exists n\,\exists a, a \in f(n).$$$
Lean4
theorem rfindOpt_dom {α} {f : ℕ → Option α} : (rfindOpt f).Dom ↔ ∃ n a, a ∈ f n :=
⟨fun h => (rfindOpt_spec ⟨h, rfl⟩).imp fun _ h => ⟨_, h⟩, fun h =>
by
have h' : ∃ n, (f n).isSome := h.imp fun n => Option.isSome_iff_exists.2
have s := Nat.find_spec h'
have fd : (rfind fun n => (f n).isSome).Dom := ⟨Nat.find h', by simpa using s.symm, fun _ _ => trivial⟩
refine ⟨fd, ?_⟩
have := rfind_spec (get_mem fd)
simpa using this⟩
