count_eq_card — Mathlib

English

The multiplicity of a in s equals the cardinality of s iff every element of s equals a.

Русский

Число вхождений a в s равно кардиналу s тогда и только тогда, когда все элементы s равны a.

LaTeX

$$$\operatorname{count}(a, s) = \operatorname{card}(s) \iff \forall x \in s,\ a = x$$$

Lean4

theorem count_eq_card {a : α} {s} : count a s = card s ↔ ∀ x ∈ s, a = x := by simp [countP_eq_card, count, @eq_comm _ a]

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