OAI/Combinatorics/SumProduct/Alignment/RationalLattice03.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RationalLattice.realPower_mem_of_coordinates line 26
  2. def OAI.RationalLattice.characterPower line 39
  3. lemma OAI.RationalLattice.character_realPower line 44
  4. theorem OAI.RationalLattice.character_kernel_pathConnected line 54
  5. theorem OAI.RationalLattice.character_kernel_inter_pathConnected line 72
  6. lemma OAI.RationalLattice.parameterEval_continuous line 105
  7. lemma OAI.RationalLattice.paramPoly_continuous line 110
  8. theorem OAI.RationalLattice.realPower_joint_continuous line 120
  9. theorem OAI.RationalLattice.contractible_of_realPower_closed line 136
  10. theorem OAI.RationalLattice.character_kernel_contractible line 158
  11. theorem OAI.RationalLattice.character_kernel_inter_contractible line 170
  12. def OAI.RationalLattice.subgroupRealPower line 190
  13. lemma OAI.RationalLattice.subgroupRealPower_continuous line 193
  14. lemma OAI.RationalLattice.subgroupRealPower_zero line 196
  15. lemma OAI.RationalLattice.subgroupRealPower_one line 199
  16. lemma OAI.RationalLattice.subgroupRealPower_add line 202
  17. def OAI.RationalLattice.subgroupCharacterPower line 208
  18. lemma OAI.RationalLattice.character_subgroupRealPower line 213
  19. lemma OAI.RationalLattice.realPower_mem_mapped_kernel line 223
  20. theorem OAI.RationalLattice.lower_kernel_inter_contractible line 237
  21. lemma OAI.TriangularDenominators.substitute_eval line 258
  22. theorem OAI.TriangularDenominators.natpow_polynomial line 266