rfind_min' — Mathlib

English

Variant form: membership of Nat.rfind p corresponds to the case analysis of p n.

Русский

Вариант: принадлежность Nat.rfind p соответствует разбору p n.

LaTeX

$$mem (Nat.rfind p) n ↔ true ∈ p n ∧ ∀ {m}, m < n → false ∈ p m$$

Lean4

theorem rfind_min' {p : ℕ → Bool} {m : ℕ} (pm : p m) : ∃ n ∈ rfind p, n ≤ m :=
  have : true ∈ (p : ℕ →. Bool) m := ⟨trivial, pm⟩
  let ⟨n, hn⟩ := dom_iff_mem.1 <| (@rfind_dom p).2 ⟨m, this, fun {_} _ => ⟨⟩⟩
  ⟨n, hn, not_lt.1 fun h => by injection mem_unique this (rfind_min hn h)⟩

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