OAI/Analysis/WeakInfiniteness/PolynomialSpan.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WeakPureInfiniteness.algebraWord_append line 23
  2. def OAI.WeakPureInfiniteness.wordMonoid line 29
  3. lemma OAI.WeakPureInfiniteness.adjoin_le_wordSpan line 36
  4. lemma OAI.WeakPureInfiniteness.exists_polynomial_of_mem_adjoin line 49
  5. lemma OAI.WeakPureInfiniteness.universal_graph_bound line 55
  6. def OAI.WeakPureInfiniteness.universalGraph line 69
  7. instance OAI.WeakPureInfiniteness.universalGraphCStar line 72
  8. def OAI.WeakPureInfiniteness.universalGraphFirst line 74
  9. lemma OAI.WeakPureInfiniteness.universalGraphFirst_isometry line 77
  10. lemma OAI.WeakPureInfiniteness.universalGraphFirst_surjective line 84
  11. def OAI.WeakPureInfiniteness.universalContractionMap line 113
  12. lemma OAI.WeakPureInfiniteness.universalContractionMap_generator line 118
  13. lemma OAI.WeakPureInfiniteness.universalContractionMap_polynomial line 128