count_nth_of_infinite

Mathlib.Data.Nat.Nth

URI: https://scilib.ai/kg/mathlib#Nat.count_nth_of_infinite

English

If the truth-set {n | p(n)} is infinite, then for every n, count p (nth p n) = n.

Русский

Если множество истинности бесконечно, то для каждого n выполняется count p (nth p n) = n.

LaTeX

$$$$ \\forall n:\\mathbb{N}, \\; \\mathrm{count}(p, \\mathrm{nth}(p, n)) = n.$$$$

Lean4

theorem count_nth_of_infinite (hp : (setOf p).Infinite) (n : ℕ) : count p (nth p n) = n :=
  count_nth fun hf => absurd hf hp

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

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

Разделы

Аффилиация

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