Prove2Me

(L : List BandRecord) : Filter.Tendsto (fun m => ledgerHi L m - ledgerLo L m) Filter.atTop (nhds 0) ↔ ledgerHi L (L.length - 1) - ledgerLo L (L.length - 1) = 0

Proved
BookProof.SirkBandLedger.ledger_width_tendsto_zero_iff

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

sirkspectral-theorytimepiece

Lean 4 theorem BookProof.SirkBandLedger.ledger_width_tendsto_zero_iff (module BookProof.SirkBandLedger), source chapter BookProof/ChapterSirkBandLedger.lean.

Preamble
-- Generated from ChapterSirkBandLedger.lean — theorem BookProof.SirkBandLedger.ledger_width_tendsto_zero_iff
import Mathlib
import Definitions.Def_ChapterSirkBandLedger
open BookProof.SirkBandLedger















open BookProof.SirkCertificateReader
open BookProof.BandEnclosure
Formal statement
theorem BookProof.SirkBandLedger.ledger_width_tendsto_zero_iff (L : List BandRecord) :
    Filter.Tendsto (fun m => ledgerHi L m - ledgerLo L m) Filter.atTop (nhds 0) ↔
      ledgerHi L (L.length - 1) - ledgerLo L (L.length - 1) = 0 := by sorry
Source
https://github.com/leonardopedrio/timepiece/blob/61595bc/BookProof/ChapterSirkBandLedger.lean

View graph