OAI/GroupTheory/SimpleAmenable/CentralCovers/FormalCoordinates.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.coordinateFactors line 15
  2. def OAI.SimpleAmenable.coordinateProjection line 38
  3. theorem OAI.SimpleAmenable.coordinateProjection_apply line 42
  4. theorem OAI.SimpleAmenable.formalMap_kill_of_actual line 55
  5. theorem OAI.SimpleAmenable.codRestrict_iSup_top line 72
  6. def OAI.SimpleAmenable.InitialCoverSystem.pairCarrierStar line 93
  7. def OAI.SimpleAmenable.InitialCoverSystem.pairCarrierConstant line 97
  8. theorem OAI.SimpleAmenable.InitialCoverSystem.pair_formal_quotient line 101
  9. theorem OAI.SimpleAmenable.star_formal_eval line 147
  10. def OAI.SimpleAmenable.formalCoordinateSource line 162
  11. def OAI.SimpleAmenable.formalCoordinateMap line 165
  12. theorem OAI.SimpleAmenable.formalCoordinate_whole line 170
  13. theorem OAI.SimpleAmenable.formalCoordinate_input line 184
  14. theorem OAI.SimpleAmenable.formal_exclusion_of_subfamily line 196
  15. theorem OAI.SimpleAmenable.formal_centralOn_of_exclusions line 213