OAI/Analysis/WeakInfiniteness/DiagonalRegular.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakPureInfiniteness.starHomCLM line 23
  2. lemma OAI.WeakPureInfiniteness.starHomCLM_apply line 29
  3. lemma OAI.WeakPureInfiniteness.groupCLM_ext line 32
  4. def OAI.WeakPureInfiniteness.rightGroupEvaluation line 41
  5. lemma OAI.WeakPureInfiniteness.rightGroupEvaluation_element line 46
  6. lemma OAI.WeakPureInfiniteness.rightGroupEvaluation_eq_zero line 54
  7. def OAI.WeakPureInfiniteness.minimalElementaryLeft line 68
  8. def OAI.WeakPureInfiniteness.minimalElementaryRight line 77
  9. lemma OAI.WeakPureInfiniteness.minimalElementaryLeft_apply line 84
  10. lemma OAI.WeakPureInfiniteness.minimalElementaryRight_apply line 87
  11. abbrev OAI.WeakPureInfiniteness.regularBase line 96
  12. lemma OAI.WeakPureInfiniteness.regularBase_eq line 100
  13. def OAI.WeakPureInfiniteness.regularPairingRight line 106
  14. def OAI.WeakPureInfiniteness.regularPairingLeft line 112
  15. lemma OAI.WeakPureInfiniteness.regularPairingRight_apply line 117
  16. lemma OAI.WeakPureInfiniteness.regularPairingLeft_apply line 122
  17. lemma OAI.WeakPureInfiniteness.freeDiagonalFunctional_regular line 131
  18. lemma OAI.WeakPureInfiniteness.freeDiagonalFunctional_elementary_kernel line 157