subset_range_nth — Mathlib

English

For any predicate p, every element x with p x lies in the range of the function n ↦ nth p n; i.e., for all x with p x there exists n with nth p n = x.

Русский

Пусть p: ℕ → ⊤. Тогда для каждого x, удовлетворяющего p x, существует n such that nth p n = x.

LaTeX

$$$\\\\forall p:\\\\mathbb{N}\\\\to \\\\mathsf{Prop},\\\\ setOf p\\\\subseteq\\\\mathrm{range}(\\\\mathrm{nth}\\\\ p).$$$

Lean4

theorem subset_range_nth : setOf p ⊆ Set.range (nth p) := fun x (hx : p x) =>
  let ⟨n, _, hn⟩ := exists_lt_card_nth_eq hx
  ⟨n, hn⟩

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