OAI/Combinatorics/HadwigerCounterexample/ConditionalProjection.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Conditional Projection

  1. def OAI.HadwigerCounterexample.dip line 13
  2. def OAI.HadwigerCounterexample.ode line 14
  3. def OAI.HadwigerCounterexample.cashbook line 15
  4. def OAI.HadwigerCounterexample.banner line 17
  5. theorem OAI.HadwigerCounterexample.ode_nonneg line 19
  6. theorem OAI.HadwigerCounterexample.ode_upper line 21
  7. theorem OAI.HadwigerCounterexample.dip_sym line 28
  8. theorem OAI.HadwigerCounterexample.dip_sub line 29
  9. theorem OAI.HadwigerCounterexample.cashbook_bound line 34
  10. theorem OAI.HadwigerCounterexample.cash_orth line 45
  11. theorem OAI.HadwigerCounterexample.ode_step line 57
  12. theorem OAI.HadwigerCounterexample.archive_gain line 73