count_finRange

Mathlib.Data.List.FinRange

URI: https://scilib.ai/kg/mathlib#List.count_finRange

English

For any a : Fin(n), the number of occurrences of a in finRange(n) is exactly 1.

Русский

Для любого a : Fin(n) количество вхождений a в finRange(n) равно 1.

LaTeX

$$$\forall {n:\mathbb{N}}\ (a:Fin\,n),\; count\ a\ (finRange\ n) = 1$$$

Lean4

@[simp]
theorem count_finRange {n : ℕ} (a : Fin n) : count a (finRange n) = 1 := by simp [count_eq_of_nodup (nodup_finRange n)]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru