OAI/Combinatorics/HadwigerCounterexample/AdditionalProbeBounds.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Additional Probe Bounds

  1. def OAI.HadwigerCounterexample.moreMatrix line 13

    Also declared: OAI/Combinatorics/HadwigerCounterexample/InjectionWitnesses.lean:12 (same declaration text).

  2. theorem OAI.HadwigerCounterexample.moreMatrix_act line 17

    Also declared: OAI/Combinatorics/HadwigerCounterexample/InjectionWitnesses.lean:16 (same declaration text).

  3. theorem OAI.HadwigerCounterexample.moreMatrix_inj line 25

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

  4. theorem OAI.HadwigerCounterexample.moreMatrix_mul line 45
  5. def OAI.HadwigerCounterexample.growFmt line 55
  6. theorem OAI.HadwigerCounterexample.grow_sum line 58
  7. def OAI.HadwigerCounterexample.growing line 61
  8. theorem OAI.HadwigerCounterexample.castMat_inj line 68
  9. theorem OAI.HadwigerCounterexample.castMat_prod line 73
  10. theorem OAI.HadwigerCounterexample.growth_inj line 79
  11. theorem OAI.HadwigerCounterexample.growth_value line 92
  12. theorem OAI.HadwigerCounterexample.column_observe line 106
  13. abbrev OAI.HadwigerCounterexample.Bazaar.Catalog line 113
  14. def OAI.HadwigerCounterexample.Bazaar.atList line 116
  15. def OAI.HadwigerCounterexample.Bazaar.probed line 121
  16. theorem OAI.HadwigerCounterexample.Bazaar.extend_probe line 124