OAI/Analysis/WeakInfiniteness/FreeFiniteRepresentations.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakPureInfiniteness.freeOrbitSpace line 28
  2. instance OAI.WeakPureInfiniteness.freeOrbitSpace_finite line 31
  3. lemma OAI.WeakPureInfiniteness.freeOrbitSpace_mem line 36
  4. lemma OAI.WeakPureInfiniteness.freeOrbitSpace_base line 40
  5. def OAI.WeakPureInfiniteness.extendUnitaryOn line 44
  6. lemma OAI.WeakPureInfiniteness.extendUnitaryOn_apply line 55
  7. lemma OAI.WeakPureInfiniteness.extendUnitaryOn_symm_apply line 61
  8. def OAI.WeakPureInfiniteness.freeFiniteRepresentation line 73
  9. lemma OAI.WeakPureInfiniteness.freeFiniteRepresentation_of line 77
  10. lemma OAI.WeakPureInfiniteness.freeFiniteRepresentation_word line 82
  11. lemma OAI.WeakPureInfiniteness.freeFiniteRepresentation_ball line 106
  12. lemma OAI.WeakPureInfiniteness.norm_freePolynomial_le_of_finite_tests line 112