{lo hi : ℕ → ℝ} {lam : ℝ} (hmem : ∀ m, lam ∈ Set.Icc (lo m) (hi m)) (hwidth : Tendsto (fun m => hi m - lo m) atTop (𝓝 0)) : Tendsto lo atTop (𝓝 lam) ∧ Tendsto hi atTop (𝓝 lam)

Initializing...

{lo hi : ℕ → ℝ} {lam : ℝ} (hmem : ∀ m, lam ∈ Set.Icc (lo m) (hi m)) (hwidth : Tendsto (fun m => hi m - lo m) atTop (𝓝 0)) : Tendsto lo atTop (𝓝 lam) ∧ Tendsto hi atTop (𝓝 lam) · Prove2Me