Library Combi.SSRcomplements.permcomp: Complement on permutations
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype div.
From mathcomp Require Import finset fingroup perm morphism action.
Set Implicit Arguments.
Import GroupScope.
From mathcomp Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype div.
From mathcomp Require Import finset fingroup perm morphism action.
Set Implicit Arguments.
Import GroupScope.
Section PermComp.
Variable T : finType.
Implicit Type (s : {perm T}) (X : {set T}) (P : {set {set T}}).
Lemma permKP s : reflect (involutive s) (s^-1 == s).
End PermComp.
Section SetAct.
Variables (aT : finGroupType) (D : {set aT}) (rT : finType) (to : action D rT).
Variable T : finType.
Implicit Type (s : {perm T}) (X : {set T}) (P : {set {set T}}).
Lemma permKP s : reflect (involutive s) (s^-1 == s).
End PermComp.
Section SetAct.
Variables (aT : finGroupType) (D : {set aT}) (rT : finType) (to : action D rT).
TODO: complete setactU, setactI, setactD ... and submit to mathcomp
Lemma setact0 a : to^* set0 a = set0.
Lemma setact1 x a : to^* [set x] a = [set to x a].
Lemma setactI S T a : to^* (S :&: T) a = to^* S a :&: to^* T a.
Lemma setactU S T a : to^* (S :|: T) a = to^* S a :|: to^* T a.
Lemma setactU1 x T a : to^* (x |: T) a = to x a |: to^* T a.
Lemma setactC S a : to^* (~: S) a = ~: to^* S a.
End SetAct.
Lemma setact1 x a : to^* [set x] a = [set to x a].
Lemma setactI S T a : to^* (S :&: T) a = to^* S a :&: to^* T a.
Lemma setactU S T a : to^* (S :|: T) a = to^* S a :|: to^* T a.
Lemma setactU1 x T a : to^* (x |: T) a = to x a |: to^* T a.
Lemma setactC S a : to^* (~: S) a = ~: to^* S a.
End SetAct.