English
Characterization of membership in Nat.rfind p: n ∈ Nat.rfind p iff p(n) = true and ∀ m < n, p(m) = false.
Русский
Характеризация принадлежности n к Nat.rfind p: n ∈ Nat.rfind p эквивалентно p(n)=true и ∀ m < n, p(m)=false.
LaTeX
$$n ∈ rfind p ↔ true ∈ p n ∧ ∀ {m}, m < n → false ∈ p m$$
Lean4
@[simp]
theorem mem_rfind {p : ℕ →. Bool} {n : ℕ} : n ∈ rfind p ↔ true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m :=
⟨fun h => ⟨rfind_spec h, @rfind_min _ _ h⟩, fun ⟨h₁, h₂⟩ =>
by
let ⟨m, hm⟩ := dom_iff_mem.1 <| (@rfind_dom p).2 ⟨_, h₁, fun {m} mn => (h₂ mn).fst⟩
rcases lt_trichotomy m n with (h | h | h)
· injection mem_unique (h₂ h) (rfind_spec hm)
· rwa [← h]
· injection mem_unique h₁ (rfind_min hm h)⟩
