OAI/Analysis/LipschitzHilbert/Trees/SourceReferenceBandAll.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Recentring an entire already-selected top family preserves its physical length bands. Only the literal short-cone membership is needed.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.referenceFamily_physicalMaskedBand_all line 15