OAI/Combinatorics/SumProduct/Alignment/FiniteMenu01.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SourceFiniteMenu.productLattice line 32
  2. def OAI.SourceFiniteMenu.quotientPi line 36
  3. lemma OAI.SourceFiniteMenu.quotientPi_mk line 45
  4. lemma OAI.SourceFiniteMenu.quotientPi_bijective line 49
  5. lemma OAI.SourceFiniteMenu.quotientPi_continuous line 63
  6. def OAI.SourceFiniteMenu.quotientPiHomeomorph line 67
  7. lemma OAI.SourceFiniteMenu.quotientPiHomeomorph_mk line 80
  8. lemma OAI.SourceFiniteMenu.product_step line 85
  9. def OAI.SourceFiniteMenu.productMetric line 99
  10. lemma OAI.SourceFiniteMenu.productMetric_compatible line 103
  11. lemma OAI.SourceFiniteMenu.quotientPi_isometry line 107
  12. lemma OAI.SourceFiniteMenu.projection_lipschitz line 116
  13. def OAI.SourceFiniteMenu.paddedObservable line 128
  14. lemma OAI.SourceFiniteMenu.paddedObservable_apply line 133
  15. lemma OAI.SourceFiniteMenu.padded_orbit line 138
  16. lemma OAI.SourceFiniteMenu.padded_lipschitz line 144
  17. theorem OAI.SourceFiniteMenu.finite_menu_padding line 160
  18. lemma OAI.SourceFiniteMenu.product_compact line 189
  19. def OAI.SourceFiniteMenu.subgroupPiHomeomorph line 195
  20. lemma OAI.SourceFiniteMenu.product_discrete line 206
  21. def OAI.SourceProductChart.key line 230
  22. lemma OAI.SourceProductChart.key_injective line 233
  23. def OAI.SourceProductChart.Index line 242
  24. instance OAI.SourceProductChart.(instance at line 243) line 243
  25. def OAI.SourceProductChart.sortedOrder line 245
  26. def OAI.SourceProductChart.orderedEnumeration line 248
  27. def OAI.SourceProductChart.enumeration line 254
  28. lemma OAI.SourceProductChart.enumeration_local line 257
  29. lemma OAI.SourceProductChart.enumeration_weights line 271
  30. def OAI.SourceProductChart.filtration line 284
  31. lemma OAI.SourceProductChart.filtration_mem line 300
  32. lemma OAI.SourceProductChart.filtration_top line 304
  33. lemma OAI.SourceProductChart.filtration_bot line 309
  34. def OAI.SourceProductChart.product line 318