OAI/Analysis/WeakInfiniteness/UniversalMapping.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakPureInfiniteness.algebraWord line 24
  2. def OAI.WeakPureInfiniteness.algebraPolynomial line 28
  3. lemma OAI.WeakPureInfiniteness.map_algebraWord line 31
  4. lemma OAI.WeakPureInfiniteness.map_algebraPolynomial line 37
  5. lemma OAI.WeakPureInfiniteness.algebraWord_operator line 41
  6. lemma OAI.WeakPureInfiniteness.algebraWord_universal line 49
  7. lemma OAI.WeakPureInfiniteness.algebraPolynomial_universal line 55
  8. lemma OAI.WeakPureInfiniteness.algebraPolynomial_operator line 59
  9. lemma OAI.WeakPureInfiniteness.norm_finitePolynomial_le_universal line 64
  10. lemma OAI.WeakPureInfiniteness.norm_operatorPolynomial_le_universal line 92
  11. lemma OAI.WeakPureInfiniteness.norm_algebraPolynomial_le_universal line 109