Checkpoint interface and its construction from an enumeration

structure GenLimit.FiniteWitness.Simplified.Checkpoints (α : Type u_2) : Type u_2

The semantic properties of the first k elements in one fixed enumeration.

• points : Set α → ℕ → Finset α

  The finite initial segments assigned to each target language.

• subset (L : Set α) (k : ℕ) : ↑(self.points L k) ⊆ L
• card {L : Set α} : L.Infinite → ∀ (k : ℕ), (self.points L k).card = k
• exhaust (L : Set α) (x : α) : x ∈ L → ∃ (k : ℕ), x ∈ self.points L (k + 1)
• agree {L : Set α} : L.Infinite → ∀ {S : Finset α} {j k : ℕ}, ↑S ⊆ L → self.points L k ⊆ S → j ≤ k → self.points (↑S) j = self.points L j

noncomputable def GenLimit.FiniteWitness.Simplified.orderedCheckpoints {α : Type u_1} (e : α ≃ ℕ) : Checkpoints α

Transport the first natural-number points along a fixed equivalence.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GenLimit.FiniteWitness.Simplified.naturalCheckpoints : Checkpoints ℕ

Checkpoints in the usual ordering of the natural numbers.

Equations

• GenLimit.FiniteWitness.Simplified.naturalCheckpoints = GenLimit.FiniteWitness.Simplified.orderedCheckpoints (Equiv.refl ℕ)

@[simp]

theorem GenLimit.FiniteWitness.Simplified.naturalCheckpoints_points (L : Set ℕ) (k : ℕ) : naturalCheckpoints.points L k = firstPoints L k