OAI/Combinatorics/Progressions/Geometry/AllocatedExternalCandidateSpatialNativeReindex.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.reindex line 51
  2. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.reindex_nativeValue line 83
  3. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.reindex_native line 86
  4. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.reindex_η line 89
  5. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.reindex_sourceChart line 92
  6. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.reindex_sourceCandidate line 95
  7. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.reindex_correlation line 98
  8. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.reindex_jointOrbit line 101
  9. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.positiveMassRetract line 104
  10. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.positiveMassRetract_mem line 113
  11. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.extend line 124
  12. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.extend_nativeValue line 128
  13. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.extend_native line 131
  14. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.extend_η line 134
  15. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.extend_sourceChart line 137
  16. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.extend_sourceCandidate line 142
  17. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.extend_correlation line 147
  18. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.extend_jointOrbit line 152