find_eq_none_iff — Mathlib

English

No index satisfies p if find returns none.

Русский

Нет индекса, который удовлетворял бы p, если find вернул none.

LaTeX

$$$$ \text{find } p = \text{none} \iff \forall i, \neg p i $$$$

Lean4

/-- `find p` returns `none` if and only if `p i` never holds. -/
theorem find_eq_none_iff {n : ℕ} {p : Fin n → Prop} [DecidablePred p] : find p = none ↔ ∀ i, ¬p i := by
  rw [← not_exists, ← isSome_find_iff]; cases find p <;> simp

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