OAI/Combinatorics/EuclideanRamsey/Transitive.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Finite transitive Euclidean configurations and their subsets are Ramsey.

  1. def OAI.EuclideanRamsey.TransitiveConsequence.distancePermutationGroup line 12
  2. instance OAI.EuclideanRamsey.TransitiveConsequence.distancePermutationFintype line 25
  3. def OAI.EuclideanRamsey.TransitiveConsequence.IsTransitive line 28
  4. theorem OAI.EuclideanRamsey.TransitiveConsequence.orbit_sum_eq line 31
  5. theorem OAI.EuclideanRamsey.TransitiveConsequence.averaged_realCriterion line 48
  6. theorem OAI.EuclideanRamsey.TransitiveConsequence.isometric_subconfiguration_ramsey line 117
  7. theorem OAI.EuclideanRamsey.TransitiveConsequence.subset_of_finite_transitive_ramsey line 136

    Distinct definitions of this name: ComparatorChallenges/EuclideanRamseyTransitive.lean:19 (same statement text; different proof or body). Qualify references as OAI.EuclideanRamsey.TransitiveConsequence.subset_of_finite_transitive_ramsey@path.