rfind_dom' — Mathlib

English

A variant: (rfind p).Dom is equivalent to ∃ n with p n = true and ∀ m ≤ n, p m is defined.

Русский

Вариант: (rfind p).Dom эквивалентен существованию n с p(n)=true и ∀ m ≤ n, p(m) определено.

LaTeX

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

Lean4

theorem rfind_dom' {p : ℕ →. Bool} : (rfind p).Dom ↔ ∃ n, true ∈ p n ∧ ∀ {m : ℕ}, m ≤ n → (p m).Dom :=
  exists_congr fun _ =>
    and_congr_right fun pn =>
      ⟨fun H _ h => (Decidable.eq_or_lt_of_le h).elim (fun e => e.symm ▸ pn.fst) (H _), fun H _ h => H (le_of_lt h)⟩

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