OAI/Analysis/LipschitzHilbert/Trees/SourceEnclosingScale.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.SourceLabeledLattice.exists_enclosing_scale line 13