rfind_dom — Mathlib

English

(rfind p).Dom holds iff there exists n with p n = true and p m defined for all m < n.

Русский

Область определения rfind p эквивалентна существованию n, такого что p(n)=true и все p(m) для m<n определены.

LaTeX

$$(rfind p).Dom ↔ ∃ n, true ∈ p n ∧ ∀ {m}, m < n → (p m).Dom$$

Lean4

@[simp]
theorem rfind_dom {p : ℕ →. Bool} : (rfind p).Dom ↔ ∃ n, true ∈ p n ∧ ∀ {m : ℕ}, m < n → (p m).Dom :=
  Iff.rfl

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