OAI/Analysis/LipschitzHilbert/Trees/SourceUnsignedSizeMonotone.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Unsigned size decreases under removing packets.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.unsignedSizeTestEnergy_mono line 14