両側剰余類

1：$x=exe\in HxK$ なので反射律が成り立つ。$y=hxk$ なら $x=h^{-1}yk^{-1}\in HyK$ なので対称律が成り立つ。$y=hxk$、$z=h'yk'$ なら $z=(h'h)x(kk')\in HxK$ なので推移律が成り立つ。$H,K$ が積と逆元で閉じていることを使った。$x$ の同値類は定義により $HxK$ である。残りは同値類の一般的な性質による（同値関係 の記事の定理「同値関係と分割の対応」）。
2：1 により、$y\in HxK$ は $y$ と $x$ が同じ同値類に属すること、すなわち $HyK=HxK$ と同値である。
3：定義から $HxK=\bigcup_{h\in H}\{hxk\mid k\in K\}=\bigcup_{h\in H}hxK$ である。右剰余類についても同様である。
4：$(hxk)^{-1}=k^{-1}x^{-1}h^{-1}$ であり、$h,k$ がそれぞれ $H,K$ を動くとき $h^{-1},k^{-1}$ も $H,K$ 全体を動くので、$g\mapsto g^{-1}$ は $HxK$ を $Kx^{-1}H$ の上に写す。この写像は自分自身が逆写像である全単射なので、制限も全単射である。$HxK=HyK$ なら、その逆元の集合として $Kx^{-1}H=Ky^{-1}H$ なので、対応は代表元によらない。逆向きの対応も同じ形なので全単射である。$\square$

1：左剰余類 $yK$ が $HxK$ に含まれるとすると $y\in HxK$ なので $y=hxk$ と書け、$yK=hxkK=hxK$ は $xK$ の $H$ 軌道に属する。逆に $hxK\subseteq HxK$ は明らかである。よって $HxK$ に含まれる左剰余類の全体は $H\cdot xK$ であり、prop-dcs-partition の 3 により $HxK$ はその和集合である。$HxK$ と $HyK$ が異なれば交わらないので、それぞれに含まれる左剰余類の集合も交わらず、対応する軌道は異なる。すべての軌道は $H\cdot yK$ の形なので $HyK$ の像であり、対応は全単射である。
2：$h\in H$ について、$hxK=xK$ は $x^{-1}hx\in K$、すなわち $h\in xKx^{-1}$ と同値である（剰余類 の記事の命題「剰余類による分割」の 2）。よって安定化群は $H\cap xKx^{-1}$ である。群の作用 の記事の定理「軌道・安定化群定理」により、軌道 $H\cdot xK$ の元の個数（濃度）は $[H:H\cap xKx^{-1}]$ に等しく、1 によりこれが $HxK$ に含まれる左剰余類の個数である。
3：$HxK$ は互いに交わらない $[H:H\cap xKx^{-1}]$ 個の左剰余類の和集合であり、各左剰余類は $|K|$ 個の元をもつ。$H$ が有限なので Lagrange の定理により $[H:H\cap xKx^{-1}]=|H|/|H\cap xKx^{-1}|$ である（Lagrangeの定理）。後半は、prop-dcs-partition の 4 により $|HxK|=|Kx^{-1}H|$ であり、前半を $(K,H,x^{-1})$ に当てると $|Kx^{-1}H|=[K:K\cap x^{-1}Hx]\,|H|$ となることから従う。$\square$

thm-dcs-orbit の 1 により、$G/K$ は $H$ 軌道 $H\cdot xK$（$x\in R$）の交わりのない和集合であり、同 2 により各軌道の元の個数は $[H:H\cap xKx^{-1}]$ である。後半は prop-dcs-partition の 1 と thm-dcs-orbit の 3 による。$\square$

1：まず、$X$ のどの $G$ 軌道も第 1 成分が $H=eH$ の点を含む。実際 $(yH,zK)=y\cdot(H,y^{-1}zK)$ である。次に、第 1 成分が $H$ の 2 点 $(H,xK)$ と $(H,x'K)$ が同じ $G$ 軌道に属するのは、$gH=H$ かつ $gxK=x'K$ となる $g$ があるとき、すなわち $x'K=gxK$ となる $g\in H$ があるときであり、これは $x'K$ が $xK$ の $H$ 軌道に属することと同値である。thm-dcs-orbit の 1 により、これは $Hx'K=HxK$ と同値である。この同値の「$\Leftarrow$」から写像は代表元によらず、「$\Rightarrow$」から単射であり、最初の注意から全射である。
2：群の作用 の記事の命題「軌道の個数の公式」を $G$ の $X$ への作用に当てる。$g$ が $X$ で動かさない点は、$G/H$ で動かさない点と $G/K$ で動かさない点の組なので、その個数は $\pi_H(g)\pi_K(g)$ である。1 により軌道の個数は $|H\backslash G/K|$ に等しいので、最初の等式を得る。2 つ目の等式は、同じ命題を $H$ の $G/K$ への作用に当て、thm-dcs-orbit の 1 を使えばよい。$\square$

$S_n$ は $k$ 元部分集合の全体 $\mathcal{P}_k$ に $\sigma\cdot A:=\sigma(A)$ で推移的に作用し（どの $k$ 元部分集合も $A_0$ の像である）、$A_0$ の安定化群は $K$ である。軌道・安定化群定理により $\sigma K\mapsto\sigma(A_0)$ は $S_n/K$ から $\mathcal{P}_k$ への全単射で、$S_n$ の作用と両立する。よって thm-dcs-orbit の 1 により、$K\sigma K=K\tau K$ は $\sigma(A_0)$ と $\tau(A_0)$ が同じ $K$ 軌道に属することと同値である。
$K$ の元は $A_0$ と補集合 $A_0^c$ をそれぞれ保つので、$|B\cap A_0|$ は $B\in\mathcal{P}_k$ の $K$ 軌道の上で一定である。逆に $|B\cap A_0|=|B'\cap A_0|=j$ なら、$|B\cap A_0^c|=|B'\cap A_0^c|=k-j$ なので、$B\cap A_0$ を $B'\cap A_0$ に写す $A_0$ の置換と、$B\cap A_0^c$ を $B'\cap A_0^c$ に写す $A_0^c$ の置換を合わせた $K$ の元が $B$ を $B'$ に写す。よって $K$ 軌道は $j=|B\cap A_0|$ で分類される。$j$ のとりうる値は $0\le j\le k$ かつ $k-j\le n-k$ を満たす整数、すなわち $\max\{0,2k-n\}\le j\le k$ のすべてであり、その個数は $\min\{k,n-k\}+1$ である。$\square$