countP_lt_length_iff — Mathlib

English

For any list l and predicate p, countP p l is less than length(l) exactly when there exists an element of l on which p is false.

Русский

Для любого списка l и предиката p число ложных значений p на элементах l меньше длины l тогда и только тогда существует элемент списка, на котором p даёт false.

LaTeX

$$$l.countP\\ p < |l| \\iff \\exists a\\in l, p(a)=\\text{false}$$$

Lean4

@[simp]
theorem countP_lt_length_iff {l : List α} {p : α → Bool} : l.countP p < l.length ↔ ∃ a ∈ l, p a = false := by
  simp [Nat.lt_iff_le_and_ne, countP_le_length]

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