OAI/Combinatorics/HadwigerCounterexample/SparseLabelBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Sparse Label Bounds

  1. abbrev OAI.HadwigerCounterexample.LabVals line 13
  2. def OAI.HadwigerCounterexample.labcomb line 15
  3. theorem OAI.HadwigerCounterexample.labcomb_eval line 19
  4. def OAI.HadwigerCounterexample.labV line 22
  5. def OAI.HadwigerCounterexample.withinL line 25
  6. theorem OAI.HadwigerCounterexample.within_eq line 28
  7. theorem OAI.HadwigerCounterexample.labV_mono line 37
  8. theorem OAI.HadwigerCounterexample.labV_unique line 41
  9. def OAI.HadwigerCounterexample.protectedBy line 55

    Source documentation

    L is the set excluded at this projected space.

    def protectedBy (p : Shape) {n} (S : Space (Ray p n)) (q : ℕ) (L : Finset (Label p.b)) :=
…

    Mentions: OAI.HadwigerCounterexample.Shape, OAI.HadwigerCounterexample.Space, OAI.HadwigerCounterexample.Ray, OAI.HadwigerCounterexample.Label

  10. theorem OAI.HadwigerCounterexample.protect_labels line 59