English
If f is monotone with respect to membership, then a ∈ rfindOpt f iff ∃ n, a ∈ f(n).
Русский
Если f монотонна по включениям, то a ∈ rfindOpt f тогда и только тогда, когда существует n, такое что a ∈ f(n).
LaTeX
$$$\bigl( \forall a,m,n,\ m \le n \to a \in f(m) \to a \in f(n) \bigr) \\Rightarrow \\bigl( a \in \mathrm{rfindOpt}(f) \iff \exists n, a \in f(n) \bigr).$$$
Lean4
theorem rfindOpt_mono {α} {f : ℕ → Option α} (H : ∀ {a m n}, m ≤ n → a ∈ f m → a ∈ f n) {a} :
a ∈ rfindOpt f ↔ ∃ n, a ∈ f n :=
⟨rfindOpt_spec, fun ⟨n, h⟩ => by
have h' := rfindOpt_dom.2 ⟨_, _, h⟩
obtain ⟨k, hk⟩ := rfindOpt_spec ⟨h', rfl⟩
have := (H (le_max_left _ _) h).symm.trans (H (le_max_right _ _) hk)
simp at this; simp [this, get_mem]⟩
