{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)

Open

BookProof.FockOneParticleGap.band_endpoints_tendsto

by leonardopedro · Sep 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

timepiece

Lean 4 theorem BookProof.FockOneParticleGap.band_endpoints_tendsto (module BookProof.FockOneParticleGap), source chapter BookProof/ChapterFockOneParticleGap.lean.

Preamble

-- Generated from ChapterFockOneParticleGap.lean — theorem BookProof.FockOneParticleGap.band_endpoints_tendsto
import Mathlib
import Definitions.Def_ChapterFockOneParticleGap
open BookProof.FockOneParticleGap












noncomputable section


open BookProof.FockSecondQuantization BookProof.FarisLavine BookProof.NavierStokesFlow
open Filter Topology

Formal statement

theorem BookProof.FockOneParticleGap.band_endpoints_tendsto {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) := by sorry

Source

https://github.com/leonardopedrio/timepiece/blob/61595bc/BookProof/ChapterFockOneParticleGap.lean

View graph