OAI/CategoryTheory/ThickClosure/PeriodicDual.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HahnWilson.PeriodicDual.cell line 18
  2. def OAI.HahnWilson.PeriodicDual.DualGhost line 23
  3. abbrev OAI.HahnWilson.PeriodicDual.BasisIndex line 36
  4. def OAI.HahnWilson.PeriodicDual.coordinate line 38
  5. def OAI.HahnWilson.PeriodicDual.coordinateFan line 48
  6. def OAI.HahnWilson.PeriodicDual.coordinateLift line 51
  7. def OAI.HahnWilson.PeriodicDual.coordinateFanIsLimit line 71
  8. theorem OAI.HahnWilson.PeriodicDual.dualGhost_free_zero_inst line 105
  9. theorem OAI.HahnWilson.PeriodicDual.dualGhost_free_zero line 123
  10. lemma OAI.HahnWilson.PeriodicDual.DualGhost.comp_right line 132
  11. def OAI.HahnWilson.PeriodicDual.cellShiftIso line 145
  12. lemma OAI.HahnWilson.PeriodicDual.dualGhost_iff line 157