OAI/Combinatorics/EuclideanRamsey/UltrafilterStrings.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.EuclideanRamsey.pure_mul_ultra line 32
  2. lemma OAI.EuclideanRamsey.mul_pure_ultra line 38
  3. def OAI.EuclideanRamsey.ultrafilterMonoid line 45
  4. inductive OAI.EuclideanRamsey.UltraColumn line 59
  5. def OAI.EuclideanRamsey.UltraColumn.value line 65
  6. def OAI.EuclideanRamsey.UltraColumn.Realizes line 68
  7. lemma OAI.EuclideanRamsey.UltraColumn.choose line 72
  8. theorem OAI.EuclideanRamsey.UltraColumn.simultaneously_realize line 85
  9. inductive OAI.EuclideanRamsey.ColumnPath line 117
  10. lemma OAI.EuclideanRamsey.ColumnPath.realizes line 124
  11. lemma OAI.EuclideanRamsey.Path.expand line 159
  12. lemma OAI.EuclideanRamsey.ColumnPath.flatten line 180
  13. lemma OAI.EuclideanRamsey.flattened_ultra_product line 190