OAI/Analysis/LipschitzHilbert/Packets/PacketDataSelectedReference.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

A selected tree from an unrestricted packet lattice has a genuine bounded reference lattice. Only the selected packets are present, and their original physical waves are preserved.

  1. def OAI.LipschitzHilbert.PacketLatticeData.selectedLabels line 16
  2. def OAI.LipschitzHilbert.PacketLatticeData.selectedOriginalLabel line 20
  3. def OAI.LipschitzHilbert.PacketLatticeData.SelectedItem line 23
  4. instance OAI.LipschitzHilbert.PacketLatticeData.selectedItemFintype line 26
  5. theorem OAI.LipschitzHilbert.PacketLatticeData.selectedLabel_has_packet line 30
  6. theorem OAI.LipschitzHilbert.PacketLatticeData.selectedItem_mem line 35
  7. theorem OAI.LipschitzHilbert.PacketLatticeData.selectedLabel_near line 45
  8. def OAI.LipschitzHilbert.PacketLatticeData.selectedReference line 50
  9. def OAI.LipschitzHilbert.PacketLatticeData.selectedReferenceEquiv line 94
  10. theorem OAI.LipschitzHilbert.PacketLatticeData.selectedReference_actualX line 104
  11. theorem OAI.LipschitzHilbert.PacketLatticeData.selectedReference_actualZ line 108
  12. theorem OAI.LipschitzHilbert.PacketLatticeData.selectedReference_physicalPacket line 116
  13. theorem OAI.LipschitzHilbert.PacketLatticeData.selectedReference_sum line 136
  14. theorem OAI.LipschitzHilbert.PacketLatticeData.selectedReference_card line 145