OAI/Combinatorics/HadwigerCounterexample/NominalSpaces.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Nominal Spaces

  1. def OAI.HadwigerCounterexample.onSide line 15
  2. def OAI.HadwigerCounterexample.putFull line 16
  3. instance OAI.HadwigerCounterexample.jointDecidableEq line 20
  4. abbrev OAI.HadwigerCounterexample.Chan line 22
  5. def OAI.HadwigerCounterexample.IP line 23
  6. def OAI.HadwigerCounterexample.IH line 25
  7. theorem OAI.HadwigerCounterexample.IP_self line 28
  8. theorem OAI.HadwigerCounterexample.IH_self line 31
  9. theorem OAI.HadwigerCounterexample.IP_IH line 34
  10. theorem OAI.HadwigerCounterexample.IP_cross line 38
  11. theorem OAI.HadwigerCounterexample.IH_cross line 41
  12. theorem OAI.HadwigerCounterexample.IH_IP line 44
  13. theorem OAI.HadwigerCounterexample.ip_decomp line 48
  14. theorem OAI.HadwigerCounterexample.images_ip line 57
  15. theorem OAI.HadwigerCounterexample.images_ih line 61
  16. def OAI.HadwigerCounterexample.sPin line 66
  17. def OAI.HadwigerCounterexample.hPin line 69
  18. def OAI.HadwigerCounterexample.halfTable line 73

    Source documentation

    small table-coordinate space J.

    def halfTable (s : Plan p n) (z : Place p) (i : Bool) :=
…

    Mentions: OAI.HadwigerCounterexample.Plan, OAI.HadwigerCounterexample.Place

  19. def OAI.HadwigerCounterexample.tabSpace line 75
  20. theorem OAI.HadwigerCounterexample.half_le_table line 78
  21. theorem OAI.HadwigerCounterexample.channel_le_table line 83
  22. theorem OAI.HadwigerCounterexample.tab_mem line 86
  23. theorem OAI.HadwigerCounterexample.pin_le_table line 110
  24. def OAI.HadwigerCounterexample.effective line 114

    Source documentation

    effective test space on endpoint i.

    def effective (s : Plan p n) (i : Bool) : Space (Profile p n) :=
…

    Mentions: OAI.HadwigerCounterexample.Plan, OAI.HadwigerCounterexample.Space, OAI.HadwigerCounterexample.Profile

  25. theorem OAI.HadwigerCounterexample.effective_mem line 117
  26. theorem OAI.HadwigerCounterexample.sPin_dim line 121
  27. theorem OAI.HadwigerCounterexample.hPin_dim line 123
  28. theorem OAI.HadwigerCounterexample.sPin_sum line 126
  29. theorem OAI.HadwigerCounterexample.dim_le_plan line 134
  30. theorem OAI.HadwigerCounterexample.effective_rank line 138
  31. theorem OAI.HadwigerCounterexample.pi_dim_le line 144
  32. theorem OAI.HadwigerCounterexample.effective_dim line 158
  33. theorem OAI.HadwigerCounterexample.table_dim line 170
  34. theorem OAI.HadwigerCounterexample.pin_protection line 181