OAI/Combinatorics/HadwigerCounterexample/InjectionWitnesses.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Injection Witnesses

  1. def OAI.HadwigerCounterexample.moreMatrix line 12

    Also declared: OAI/Combinatorics/HadwigerCounterexample/AdditionalProbeBounds.lean:13 (same declaration text).

  2. theorem OAI.HadwigerCounterexample.moreMatrix_act line 16

    Also declared: OAI/Combinatorics/HadwigerCounterexample/AdditionalProbeBounds.lean:17 (same declaration text).

  3. theorem OAI.HadwigerCounterexample.moreMatrix_inj line 24

    Distinct definitions of this name: OAI/Combinatorics/HadwigerCounterexample/AdditionalProbeBounds.lean:25 (same statement text; different proof or body). Qualify references as OAI.HadwigerCounterexample.moreMatrix_inj@path.

  4. def OAI.HadwigerCounterexample.pushCost line 44
  5. theorem OAI.HadwigerCounterexample.booming line 47
  6. theorem OAI.HadwigerCounterexample.cannon line 131