45private noncomputable def CE : ℕ → (ℕ → ℕ) 46 | 0 => (bounded_subseq_tendsto (fun n => f n 0) c R (fun n => hf n 0)).choose 47 | m + 1 => 48 let φ := CE m
proof body
Definition body.
49 let ψ := (bounded_subseq_tendsto (fun n => f (φ n) (m + 1)) c R 50 (fun n => hf (φ n) (m + 1))).choose 51 φ ∘ ψ 52 53/-- Limit at column m. -/
used by (13)
From the project-wide theorem graph. These declarations reference this one in their body.