le_nth_count'

Mathlib.Data.Nat.Nth

URI: https://scilib.ai/kg/mathlib#Nat.le_nth_count'

← MathLib Explorer

English

If there exists k with p(k) and n ≤ k, then n ≤ nth p (count p n).

Русский

Если существует k, such что p(k) и n ≤ k, то n ≤ nth p (count p n).

LaTeX

$$$$ \\exists k:\\, p(k) \\land n \\le k \\Rightarrow n \\le \\mathrm{nth}(p, \\mathrm{count}(p,n)). $$$$

Lean4

theorem le_nth_count' {n : ℕ} (hpn : ∃ k, p k ∧ n ≤ k) : n ≤ nth p (count p n) :=
  (le_csInf hpn fun _ => And.right).trans (nth_count_eq_sInf p n).ge

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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