OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Programs/InitializedObservation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A safe rational loader transfers the periodic body's continuous-time event criterion to the fixed starting point of the initialized fluid.

  1. def OAI.ForcedComputation.fixedStart line 13
  2. theorem OAI.ForcedComputation.initialized_observation_iff line 15