temp

Author: tb65536

Mathlib/Combinatorics/Ramsey/Basic.lean

@@ -288,8 +288,9 @@ end
 
 section
 
--- todo: add more general defs for graphs in terms of `LabelingContains` and `LabelingIndContains`
--- but keep this def because it is needed to bootstrap existence of ramsey numbers for graphs
+-- todo: add two more general versions of `IsRamseyValid` for graphs in terms of `LabelingContains`
+-- and `LabelingIndContains` but keep this def because it is needed to bootstrap existence of Ramsey
+-- numbers for graphs.
 
 /-- The predicate `IsRamseyValid V n` states that the type `V` is large enough to guarantee a
 clique of size `n k` for some colour `k : K`. -/