count_univ — Mathlib

English

In a finite type α with decidable equality, each a ∈ α occurs exactly once in Finset.univ.val.

Русский

В конечном типе α с разрешимым равенством каждый элемент a встречается ровно один раз в Finset.univ.val.

LaTeX

$$$$ \\operatorname{count}(a, \\operatorname{Finset.univ}.val) = 1. $$$$

Lean4

@[simp]
theorem count_univ [DecidableEq α] (a : α) : count a Finset.univ.val = 1 :=
  count_eq_one_of_mem Finset.univ.nodup (Finset.mem_univ _)

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