Prove2Me

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

Proved
BookProof.BandEnclosure.band_enclosure_endpoints_tendsto

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

timepiece

Lean 4 theorem BookProof.BandEnclosure.band_enclosure_endpoints_tendsto (module BookProof.BandEnclosure), source chapter BookProof/ChapterBandEnclosure.lean.

Preamble
-- Generated from ChapterBandEnclosure.lean — theorem BookProof.BandEnclosure.band_enclosure_endpoints_tendsto
import Mathlib
import Definitions.Def_ChapterBandEnclosure
open BookProof.BandEnclosure










noncomputable section

open Filter Topology


open BookProof.FockOneParticleGap BookProof.FockSecondQuantization
open BookProof.ChapterH6 BookProof.ChapterH8
Formal statement
theorem BookProof.BandEnclosure.band_enclosure_endpoints_tendsto {lo hi a : ℕ → ℝ} {lam : ℝ}
    (hnest : NestedBands lo hi) (hmem : ∀ m, a m ∈ Set.Icc (lo m) (hi m))
    (hconv : Tendsto a atTop (𝓝 lam))
    (hwidth : Tendsto (fun m => hi m - lo m) atTop (𝓝 0)) :
    (∀ m, lam ∈ Set.Icc (lo m) (hi m)) ∧
      (∀ lam', (∀ m, lam' ∈ Set.Icc (lo m) (hi m)) → lam' = lam) ∧
      Tendsto lo atTop (𝓝 lam) ∧ Tendsto hi atTop (𝓝 lam) := by sorry
Source
https://github.com/leonardopedrio/timepiece/blob/61595bc/BookProof/ChapterBandEnclosure.lean

View graph