OAI/Analysis/WeakInfiniteness/FreeFiniteQuotients.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakPureInfiniteness.freeWordBall line 18
  2. lemma OAI.WeakPureInfiniteness.mem_freeWordBall line 23
  3. lemma OAI.WeakPureInfiniteness.one_mem_freeWordBall line 38
  4. lemma OAI.WeakPureInfiniteness.exists_freeBallTranslation line 42
  5. def OAI.WeakPureInfiniteness.freeBallTranslation line 60
  6. lemma OAI.WeakPureInfiniteness.freeBallTranslation_apply line 64
  7. lemma OAI.WeakPureInfiniteness.freeBallTranslation_inv_apply line 69
  8. def OAI.WeakPureInfiniteness.freeFiniteQuotient line 82
  9. lemma OAI.WeakPureInfiniteness.freeFiniteQuotient_of line 86
  10. lemma OAI.WeakPureInfiniteness.free_mk_cons_pos line 91
  11. lemma OAI.WeakPureInfiniteness.free_mk_cons_neg line 95
  12. lemma OAI.WeakPureInfiniteness.freeFiniteQuotient_word_apply line 98
  13. lemma OAI.WeakPureInfiniteness.freeFiniteQuotient_apply_base line 120
  14. lemma OAI.WeakPureInfiniteness.freeFiniteQuotient_injOn_ball line 125
  15. lemma OAI.WeakPureInfiniteness.freeFiniteQuotient_injOn_finset line 133
  16. lemma OAI.WeakPureInfiniteness.eventually_freeFiniteQuotient_eq_iff line 140
  17. lemma OAI.WeakPureInfiniteness.tendsto_freeFiniteQuotient_diagonal line 151