OAI/Combinatorics/VariableWL/ExactProjection.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.VariableWL.Blocks.component_links_small line 11
  2. theorem OAI.VariableWL.Blocks.offsetFamily_restrict line 18
  3. theorem OAI.VariableWL.Blocks.choose_extension_shifts line 38
  4. theorem OAI.VariableWL.Blocks.offsetFamily_extend_strict line 84
  5. theorem OAI.VariableWL.Blocks.offsetFamily_exact_projection line 134
  6. def OAI.VariableWL.Blocks.RawValue line 159
  7. instance OAI.VariableWL.Blocks.rawValueAddCommGroup line 163
  8. instance OAI.VariableWL.Blocks.rawValueFintype line 166
  9. def OAI.VariableWL.Blocks.boundaryMap line 169
  10. def OAI.VariableWL.Blocks.inhomogeneity line 177
  11. def OAI.VariableWL.Blocks.LegalValue line 181
  12. abbrev OAI.VariableWL.Blocks.Valuation line 184
  13. instance OAI.VariableWL.Blocks.valuationFintype line 187
  14. theorem OAI.VariableWL.Blocks.legal_zero line 190
  15. theorem OAI.VariableWL.Blocks.legal_nonempty line 193
  16. def OAI.VariableWL.Blocks.translateValuation line 201
  17. def OAI.VariableWL.Blocks.valueOfReadouts line 212
  18. def OAI.VariableWL.Blocks.Carries line 217
  19. theorem OAI.VariableWL.Blocks.valueOfReadouts_carries line 227
  20. theorem OAI.VariableWL.Blocks.carries_hasReadout line 239
  21. theorem OAI.VariableWL.Blocks.carries_exists line 249
  22. theorem OAI.VariableWL.Blocks.offsetFamily_legal line 260
  23. def OAI.VariableWL.Blocks.familyList line 284
  24. theorem OAI.VariableWL.Blocks.valueOfReadouts_congr line 294
  25. def OAI.VariableWL.Blocks.OffsetLists line 303
  26. def OAI.VariableWL.Blocks.restrictList line 308
  27. theorem OAI.VariableWL.Blocks.offsetLists_nonempty line 312
  28. theorem OAI.VariableWL.Blocks.exact_projection line 318
  29. instance OAI.VariableWL.Blocks.readoutValueAddCommGroup line 339
  30. instance OAI.VariableWL.Blocks.readoutValueFintype line 342
  31. theorem OAI.VariableWL.Blocks.squareLeft_ne_right line 345
  32. theorem OAI.VariableWL.Blocks.squareBottom_ne_top line 350
  33. theorem OAI.VariableWL.Blocks.carries_unique line 355
  34. def OAI.VariableWL.Blocks.readout line 367
  35. theorem OAI.VariableWL.Blocks.readout_carries line 371
  36. theorem OAI.VariableWL.Blocks.readout_eq line 375
  37. theorem OAI.VariableWL.Blocks.carries_add line 380
  38. theorem OAI.VariableWL.Blocks.readout_add line 410
  39. theorem OAI.VariableWL.Blocks.readout_valueOfReadouts line 415
  40. theorem OAI.VariableWL.Blocks.readout_zero line 420
  41. theorem OAI.VariableWL.Blocks.offsetLists_agree line 426
  42. instance OAI.VariableWL.Blocks.horizontalFintype line 439
  43. instance OAI.VariableWL.Blocks.verticalFintype line 447
  44. instance OAI.VariableWL.Blocks.squareFintype line 455
  45. instance OAI.VariableWL.Blocks.blockFintype line 463