OAI/Analysis/LipschitzHilbert/Packets/SourceSupportedPacketData.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Raw packet data with length control only on actual retained items. No concentration conclusion is included in these structures.

  1. structure OAI.LipschitzHilbert.SupportedTopRawPacketData line 10
  2. structure OAI.LipschitzHilbert.SupportedTopCovariantData line 34
  3. structure OAI.LipschitzHilbert.SourceSupportedLatticeTopGeometry line 52
  4. structure OAI.LipschitzHilbert.SourceSupportedLabeledTopGeometry line 62