nth_mem_of_infinite — Mathlib

English

Let p: N → Prop. If the set {x ∈ N | p(x)} is infinite, then for every n ∈ N we have p(nth p n).

Русский

Пусть p: ℕ → ⊤. Если множество {x ∈ ℕ | p(x)} бесконечно, тогда для каждого n ∈ ℕ выполняется p(nth p n).

LaTeX

$$$\\\\forall p:\\\\mathbb{N}\\\\to \\\\mathsf{Prop},\\\\ #(\\\\{x \\\\in \\\\mathbb{N} \\\\mid p x\\\\})=\\\\infty \\\\Rightarrow \\\\forall n \\\\in \\\\mathbb{N},\\\\ p(\\\\mathrm{nth}\\\\ p\\\\ n).$$$

Lean4

theorem nth_mem_of_infinite (hf : (setOf p).Infinite) (n : ℕ) : p (nth p n) :=
  Set.range_subset_iff.1 (range_nth_of_infinite hf).le n

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