find_eq_some_iff — Mathlib

English

For a decidable predicate p on Fin n, Fin.find p equals some i if and only if p i holds and i is a minimal witness, i.e., for every j with p j we have i ≤ j.

Русский

Для предиката p на Fin n с разрешимостью, Fin.find p равен some i тогда и только тогда, когда p i выполняется и i является минимальным свидетелем, т.е. для каждого j с p j имеем i ≤ j.

LaTeX

$$$Fin.find p = some i \\iff p i \\ \\wedge\\ \\forall j, p j \\rightarrow i \\le j$$$

Lean4

theorem find_eq_some_iff {p : Fin n → Prop} [DecidablePred p] {i : Fin n} :
    Fin.find p = some i ↔ p i ∧ ∀ j, p j → i ≤ j :=
  mem_find_iff

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