OAI/Combinatorics/HadwigerCounterexample/ComponentIndices.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Component Indices

  1. abbrev OAI.HadwigerCounterexample.Tag line 12
  2. abbrev OAI.HadwigerCounterexample.Comp line 13
  3. def OAI.HadwigerCounterexample.edge line 17
  4. theorem OAI.HadwigerCounterexample.edge_eq line 20
  5. theorem OAI.HadwigerCounterexample.edge_symm line 23
  6. def OAI.HadwigerCounterexample.inc line 28
  7. instance OAI.HadwigerCounterexample.(instance at line 29) line 29
  8. theorem OAI.HadwigerCounterexample.inc_edge_fst line 31
  9. theorem OAI.HadwigerCounterexample.inc_edge_iff line 34
  10. abbrev OAI.HadwigerCounterexample.TagStar line 37
  11. def OAI.HadwigerCounterexample.starEquiv line 39
  12. theorem OAI.HadwigerCounterexample.card_star line 60
  13. def OAI.HadwigerCounterexample.allowed line 65

    Source documentation

    l in I_d.

    def allowed (d l : Tag g) :=
…

    Mentions: OAI.HadwigerCounterexample.Tag

  14. instance OAI.HadwigerCounterexample.(instance at line 68) line 68
  15. theorem OAI.HadwigerCounterexample.not_allowed line 71
  16. theorem OAI.HadwigerCounterexample.card_allowed line 75
  17. theorem OAI.HadwigerCounterexample.card_allowed' line 100