OAI/Combinatorics/EditApproximation/Geometry/ComparisonLiftStep.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Actual mass and energy identities at every kind of comparison-tree node.

  1. theorem OAI.EditApproximation.stoppedComparisonEnergy_step_stopped line 11
  2. theorem OAI.EditApproximation.stageComparisonMass_step_stopped line 49
  3. theorem OAI.EditApproximation.stageComparisonEnergy_step_stopped line 70
  4. theorem OAI.EditApproximation.stageComparison_step_none line 94
  5. theorem OAI.EditApproximation.stageComparisonMass_step_active line 106
  6. theorem OAI.EditApproximation.stageComparisonEnergy_step_active line 125