OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Prelude.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VelocityDetection.Prelude.rule line 19

    Also declared: ComparatorChallenges/NavierStokesVelocity.lean:484 (same declaration text).

  2. def OAI.VelocityDetection.Prelude.table' line 22

    Also declared: ComparatorChallenges/NavierStokesVelocity.lean:487 (same declaration text).

  3. def OAI.VelocityDetection.Prelude.embed line 26
  4. def OAI.VelocityDetection.Prelude.initial line 29

    Also declared: ComparatorChallenges/NavierStokesVelocity.lean:491 (same declaration text).

  5. theorem OAI.VelocityDetection.Prelude.table_cast line 31
  6. theorem OAI.VelocityDetection.Prelude.table_last line 34
  7. theorem OAI.VelocityDetection.Prelude.applyRule_embed line 37
  8. theorem OAI.VelocityDetection.Prelude.lookup_embed line 40
  9. theorem OAI.VelocityDetection.Prelude.lookup_initial line 44
  10. theorem OAI.VelocityDetection.Prelude.next_initial line 48
  11. theorem OAI.VelocityDetection.Prelude.next_embed line 55
  12. theorem OAI.VelocityDetection.Prelude.orbit_initial line 60
  13. theorem OAI.VelocityDetection.Prelude.halts_initial line 67