OAI/GroupTheory/FiniteType/SequentialLimit.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SequentialLimit.End line 11
  2. instance OAI.SequentialLimit.endFunLike line 14
  3. def OAI.SequentialLimit.transition line 20
  4. lemma OAI.SequentialLimit.transition_apply line 22
  5. instance OAI.SequentialLimit.directed line 25
  6. abbrev OAI.SequentialLimit.Limit line 34
  7. abbrev OAI.SequentialLimit.of line 36
  8. lemma OAI.SequentialLimit.of_advance line 38
  9. lemma OAI.SequentialLimit.of_succ line 41
  10. lemma OAI.SequentialLimit.of_injective line 46
  11. lemma OAI.SequentialLimit.exists_rep line 50
  12. lemma OAI.SequentialLimit.induction line 53
  13. lemma OAI.SequentialLimit.iterate_compat line 56
  14. def OAI.SequentialLimit.map line 63
  15. lemma OAI.SequentialLimit.map_of line 67
  16. def OAI.SequentialLimit.shift line 71
  17. lemma OAI.SequentialLimit.shift_of line 86
  18. lemma OAI.SequentialLimit.shift_symm_of line 89
  19. lemma OAI.SequentialLimit.shift_pow_of line 92
  20. lemma OAI.SequentialLimit.tuple_rep line 98
  21. lemma OAI.SequentialLimit.pair_rep line 106
  22. instance OAI.SequentialLimit.limitCountable line 113
  23. lemma OAI.SequentialLimit.limit_infinite line 116
  24. def OAI.SequentialLimit.stage line 119
  25. lemma OAI.SequentialLimit.stage_mono line 121
  26. lemma OAI.SequentialLimit.stage_strict line 126
  27. lemma OAI.SequentialLimit.shift_stage line 139
  28. def OAI.SequentialAction.transitionHom line 157
  29. instance OAI.SequentialAction.homDirected line 172
  30. instance OAI.SequentialAction.limitGroup line 175
  31. def OAI.SequentialAction.ofGroup line 178
  32. lemma OAI.SequentialAction.iterate_equivariant line 184
  33. def OAI.SequentialAction.act line 190
  34. lemma OAI.SequentialAction.act_of line 196
  35. def OAI.SequentialAction.limitAction line 200
  36. lemma OAI.SequentialAction.of_smul line 219
  37. lemma OAI.SequentialAction.of_mul line 223
  38. lemma OAI.SequentialAction.of_one line 226
  39. lemma OAI.SequentialAction.act_injective line 228
  40. def OAI.SequentialAction.shiftGroup line 238
  41. lemma OAI.SequentialAction.shiftGroup_of line 247
  42. lemma OAI.SequentialAction.shift_equivariant line 250
  43. def OAI.SequentialAction.HasImageTupleTransitivity line 255
  44. lemma OAI.SequentialAction.limit_tuple_transitivity line 259