First-k checkpoints, exactly as in the simplified manuscript.

noncomputable def GenLimit.FiniteWitness.Simplified.firstPoints (L : Set ℕ) (k : ℕ) : Finset ℕ

The first k elements of a natural-number set, or all its elements if fewer exist.

Equations

• GenLimit.FiniteWitness.Simplified.firstPoints L k = {x ∈ Finset.image (Nat.nth fun (n : ℕ) => n ∈ L) (Finset.range k) | x ∈ L ∧ Nat.count (fun (n : ℕ) => n ∈ L) x < k}

@[simp]

theorem GenLimit.FiniteWitness.Simplified.mem_firstPoints (L : Set ℕ) (k x : ℕ) : x ∈ firstPoints L k ↔ x ∈ L ∧ Nat.count (fun (n : ℕ) => n ∈ L) x < k

theorem GenLimit.FiniteWitness.Simplified.firstPoints_subset (L : Set ℕ) (k : ℕ) : ↑(firstPoints L k) ⊆ L

theorem GenLimit.FiniteWitness.Simplified.firstPoints_mono (L : Set ℕ) {j k : ℕ} (hjk : j ≤ k) : firstPoints L j ⊆ firstPoints L k

theorem GenLimit.FiniteWitness.Simplified.firstPoints_card {L : Set ℕ} (hL : L.Infinite) (k : ℕ) : (firstPoints L k).card = k

theorem GenLimit.FiniteWitness.Simplified.firstPoints_exhausts (L : Set ℕ) {x : ℕ} (hx : x ∈ L) : ∃ (k : ℕ), x ∈ firstPoints L (k + 1)

theorem GenLimit.FiniteWitness.Simplified.firstPoints_agree {L : Set ℕ} (hL : L.Infinite) {S : Finset ℕ} {j k : ℕ} (hSL : ↑S ⊆ L) (hseen : firstPoints L k ⊆ S) (hjk : j ≤ k) : firstPoints (↑S) j = firstPoints L j