inductive Hex.PermGroup.Kernel.Span {n : Nat} (S : Perm n → Prop) : Perm n → Prop

Generation by a predicate, for packed generators that have not yet been reified as an array of permutations. Words use left-action composition.

• id {n : Nat} {S : Perm n → Prop} : Span S (Perm.id n)
• mul_left {n : Nat} {S : Perm n → Prop} {a b : Perm n} : S a → Span S b → Span S (a.comp b)
• inv_mul_left {n : Nat} {S : Perm n → Prop} {a b : Perm n} : S a → Span S b → Span S (a.inv.comp b)

theorem Hex.PermGroup.Kernel.Span.generator {n : Nat} {S : Perm n → Prop} {p : Perm n} (hp : S p) : Span S p

theorem Hex.PermGroup.Kernel.Span.comp {n : Nat} {S : Perm n → Prop} {p q : Perm n} (hp : Span S p) (hq : Span S q) : Span S (p.comp q)

theorem Hex.PermGroup.Kernel.Span.inv {n : Nat} {S : Perm n → Prop} {p : Perm n} (hp : Span S p) : Span S p.inv

theorem Hex.PermGroup.Kernel.Span.lift {n : Nat} {S P : Perm n → Prop} (hi : P (Perm.id n)) (hs : ∀ (p : Perm n), S p → P p) (hc : ∀ (p q : Perm n), P p → P q → P (p.comp q)) (hv : ∀ (p : Perm n), P p → P p.inv) {p : Perm n} (hp : Span S p) : P p

theorem Hex.PermGroup.Kernel.Span.empty {n : Nat} {p : Perm n} : Span (fun (x : Perm n) => False) p ↔ p = Perm.id n