OAI/Analysis/LipschitzHilbert/Packets/PacketDataEnclosingScale.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Replace an arbitrary selected top length by a comparable existing dyadic scale while retaining every packet below that top.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.exists_enclosing_scale line 13