OAI/MathematicalPhysics/NavierStokes/VelocityDetection/FiniteAddresses.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.VelocityDetection.FiniteAddresses.Box line 14
  2. def OAI.VelocityDetection.FiniteAddresses.config line 16
  3. def OAI.VelocityDetection.FiniteAddresses.sourceAddress line 19
  4. theorem OAI.VelocityDetection.FiniteAddresses.sourceAddress_injective line 21
  5. theorem OAI.VelocityDetection.FiniteAddresses.sourceAddress_count line 27
  6. def OAI.VelocityDetection.FiniteAddresses.Active line 43
  7. instance OAI.VelocityDetection.FiniteAddresses.(instance at line 45) line 45
  8. def OAI.VelocityDetection.FiniteAddresses.rule line 50
  9. theorem OAI.VelocityDetection.FiniteAddresses.lookup_rule line 53
  10. def OAI.VelocityDetection.FiniteAddresses.target line 57
  11. def OAI.VelocityDetection.FiniteAddresses.targetAddress line 60
  12. theorem OAI.VelocityDetection.FiniteAddresses.target_stacks_lt line 64
  13. theorem OAI.VelocityDetection.FiniteAddresses.targetAddress_count line 68
  14. theorem OAI.VelocityDetection.FiniteAddresses.targetAddress_injective line 73