OAI/Combinatorics/HadwigerCounterexample/NumericalGramPrescriptions.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Numerical Gram Prescriptions

  1. def OAI.HadwigerCounterexample.spacePunch line 13
  2. theorem OAI.HadwigerCounterexample.punch_real line 18
  3. theorem OAI.HadwigerCounterexample.beam_rank line 40
  4. theorem OAI.HadwigerCounterexample.sharedPunch line 62
  5. def OAI.HadwigerCounterexample.creed line 68

    Source documentation

    selected pure excludes second tags

    def creed (p : Shape) (E : Finset (Tag p.g)) :=
…

    Mentions: OAI.HadwigerCounterexample.Shape, OAI.HadwigerCounterexample.Tag

  6. theorem OAI.HadwigerCounterexample.purePunch line 71