pith. machine review for the scientific record. sign in
theorem proved term proof

CE_conv_at

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  87private theorem CE_conv_at : ∀ m, Tendsto (fun n => f (CE f c R hf m n) m)
  88    atTop (𝓝 (CL f c R hf m)) := by

proof body

Term-mode proof.

  89  intro m; cases m with
  90  | zero =>
  91    exact (bounded_subseq_tendsto (fun n => f n 0) c R (fun n => hf n 0)).choose_spec.choose_spec.2
  92  | succ k => exact LE_conv f c R hf k
  93

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (6)

Lean names referenced from this declaration's body.