OAI/Combinatorics/HadwigerCounterexample/ImagePartitions.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Image Partitions

  1. theorem OAI.HadwigerCounterexample.plan_mono line 13
  2. def OAI.HadwigerCounterexample.planNew line 17

    Source documentation

    Joint nominal rank modulo pins.

    def planNew (a b : Plan p n) := planRank (a⊔b) - planRank a

    Mentions: OAI.HadwigerCounterexample.Plan, OAI.HadwigerCounterexample.planRank

  3. theorem OAI.HadwigerCounterexample.plan_add_rank line 19
  4. theorem OAI.HadwigerCounterexample.planNew_mono_add line 23
  5. def OAI.HadwigerCounterexample.Pin.make line 32
  6. theorem OAI.HadwigerCounterexample.Pin.combine line 34
  7. def OAI.HadwigerCounterexample.fee line 45
  8. def OAI.HadwigerCounterexample.Pin.clear line 46
  9. structure OAI.HadwigerCounterexample.PeelCell line 49
  10. theorem OAI.HadwigerCounterexample.heavy_leaf line 58
  11. theorem OAI.HadwigerCounterexample.peel_family line 171