def Hex.GraphIso.Aut.Orbit {n k : Nat} (G : Colored n k) (base : List (Fin n)) (u v : Fin n) : Prop

The orbit relation for the full pointwise stabilizer of a base.

Equations

• Hex.GraphIso.Aut.Orbit G base u v = ∃ (p : Hex.Perm n), Hex.GraphIso.IsIso G G p ∧ Hex.GraphIso.Perm.Fixes base p ∧ p.get u = v

theorem Hex.GraphIso.Aut.Orbit.refl {n k : Nat} (G : Colored n k) (base : List (Fin n)) (u : Fin n) : Orbit G base u u

theorem Hex.GraphIso.Aut.Orbit.trans {n k : Nat} {G : Colored n k} {base : List (Fin n)} {u v w : Fin n} (h : Orbit G base u v) (h' : Orbit G base v w) : Orbit G base u w

theorem Hex.GraphIso.Aut.Orbit.symm {n k : Nat} {G : Colored n k} {base : List (Fin n)} {u v : Fin n} (h : Orbit G base u v) : Orbit G base v u