English
For p : Fin n → Prop with decidablePred, an index i ∈ Fin n belongs to Fin.find p if and only if p i holds and, for every j with p j, we have i ≤ j. In other words, i is a minimal witness to p.
Русский
Пусть p : Fin n → Prop с разрешимым предикатом. Метрический элемент i ∈ Fin n принадлежит Fin.find p тогда и только тогда, когда p i выполняется и для любого j, если p j выполняется, то i ≤ j; то есть i – минимальный свидетель p.
LaTeX
$$$i \\in Fin.find p \\;\\Longleftrightarrow\\; p i \\ \\wedge\\ \\forall j, (p j) \\rightarrow i \\le j$$$
Lean4
theorem mem_find_iff {p : Fin n → Prop} [DecidablePred p] {i : Fin n} : i ∈ Fin.find p ↔ p i ∧ ∀ j, p j → i ≤ j :=
⟨fun hi ↦ ⟨find_spec _ hi, fun _ ↦ find_min' hi⟩, by
rintro ⟨hpi, hj⟩
cases hfp : Fin.find p
· rw [find_eq_none_iff] at hfp
exact (hfp _ hpi).elim
· exact Option.some_inj.2 (Fin.le_antisymm (find_min' hfp hpi) (hj _ (find_spec _ hfp)))⟩
