OAI/Computability/WLIdentification/StableColors.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WLIdentification.SimpleStable line 8

   Source documentation

   Stable joint colors, transported to actual finite vertex types.

   def SimpleStable {V W : Type} [Fintype V] [Fintype W]
       (G : SimpleGraph V) (H : SimpleGraph W) {k : ℕ}
       (v : Fin k → V) (w : Fin k → W) : Prop :=
   …

2. theorem OAI.WLIdentification.SimpleStable.local_info line 19
3. theorem OAI.WLIdentification.SimpleStable.extension line 36
4. def OAI.WLIdentification.TagStable line 75

   Source documentation

   Testing degree intervals converts stable uncolored tuples back into their named base classes, without assuming color information as a new WL hypothesis.

   def TagStable {V W : Type} [Fintype V] [Fintype W]
       (G : SimpleGraph V) (H : SimpleGraph W) (color : V → ℕ) (color' : W → ℕ)
       {k : ℕ} (v : Fin k → V) (w : Fin k → W) : Prop :=
   …

5. theorem OAI.WLIdentification.TagStable.colors line 86
6. theorem OAI.WLIdentification.TagStable.exists_of_equivalent line 94
7. theorem OAI.WLIdentification.TagStable.extension line 124