OAI/Analysis/LipschitzHilbert/Packets/PacketDataActualReferenceEvents.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual parent-square and continuing-path reference events of the source packet family. The union is independent of every complex phase.

  1. def OAI.LipschitzHilbert.PacketLatticeData.actualReferenceData line 29
  2. def OAI.LipschitzHilbert.PacketLatticeData.actualReferencePacketSet line 36
  3. def OAI.LipschitzHilbert.PacketLatticeData.actualReferenceSelection line 48
  4. def OAI.LipschitzHilbert.PacketLatticeData.actualReferenceBad line 57
  5. theorem OAI.LipschitzHilbert.PacketLatticeData.actualReferenceBad_measurable line 65
  6. theorem OAI.LipschitzHilbert.PacketLatticeData.actualReferencePacketSet_subset line 74
  7. theorem OAI.LipschitzHilbert.PacketLatticeData.actualReferenceBad_excludes line 81