Regular direct limits

At the regular uncountable recursion length, every point of a completed direct limit already comes from one component. This is the formal version of the manuscript's assertion that a countable Cauchy sequence is contained in one earlier stage.

theorem ScottishBook155.recursionIndex_nat_bounded (a : ℕ → RecursionIndexZero) : ∃ (j : RecursionIndexZero), ∀ (n : ℕ), a n < j

A countable family of recursion indices has a strict upper bound.

theorem ScottishBook155.RegularDirectLimit.exists_completedOf (G : RecursionIndexZero → Type) [(i : RecursionIndexZero) → NormedAddCommGroup (G i)] [(i : RecursionIndexZero) → NormedSpace ℝ (G i)] [∀ (i : RecursionIndexZero), CompleteSpace (G i)] (e : (i j : RecursionIndexZero) → i ≤ j → G i →ₗᵢ[ℝ] G j) [DirectedSystem G fun (x1 x2 : RecursionIndexZero) (x3 : x1 ≤ x2) => ⇑(e x1 x2 x3)] (z : NormedDirectLimit.CompletedCarrier G e) : ∃ (j : RecursionIndexZero) (x : G j), (NormedDirectLimit.completedOf G e j) x = z

At regular uncountable length, the canonical component embeddings jointly surject onto the completed direct limit.