OAI/Analysis/WeakInfiniteness/TensorDensity.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakPureInfiniteness.spatialElementaryLeft line 23
  2. def OAI.WeakPureInfiniteness.spatialElementaryRight line 32
  3. lemma OAI.WeakPureInfiniteness.spatialElementaryLeft_apply line 39
  4. lemma OAI.WeakPureInfiniteness.spatialElementaryRight_apply line 42
  5. lemma OAI.WeakPureInfiniteness.spatialElementary_sum_left line 45
  6. lemma OAI.WeakPureInfiniteness.spatialElementary_sum_right line 52
  7. def OAI.WeakPureInfiniteness.minimalAmbientInclusion line 59
  8. def OAI.WeakPureInfiniteness.groupTensorPolynomial line 73
  9. lemma OAI.WeakPureInfiniteness.groupTensorPolynomial_val line 77
  10. lemma OAI.WeakPureInfiniteness.groupTensorPolynomial_dense line 86