count_lt_length_iff — Mathlib

English

Over a list l with decidable equality, count of a in l is strictly less than length(l) iff there exists some element of l not equal to a.

Русский

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

LaTeX

$$$l.count\\ a < |l| \\iff \\exists b\\in l, b \\neq a$$$

Lean4

@[simp]
theorem count_lt_length_iff {a : α} : l.count a < l.length ↔ ∃ b ∈ l, b ≠ a := by simp [count]

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