Step
*
1
2
of Lemma
two-factorizations-no-repeats
1. n : ℕ
⊢ Inj({x:{x:ℤ| (1 ≤ x) ∧ x < n + 1} | (x ∈ filter(λa.(n rem a =z 0);[1, n + 1)))} ℤ × ℤ;λa.<a, n ÷ a>)
BY
{ (D 0 THEN Reduce 0 THEN Auto) }
Latex:
Latex:
1.  n  :  \mBbbN{}
\mvdash{}  Inj(\{x:\{x:\mBbbZ{}|  (1  \mleq{}  x)  \mwedge{}  x  <  n  +  1\}  |  (x  \mmember{}  filter(\mlambda{}a.(n  rem  a  =\msubz{}  0);[1,  n  +  1)))\}  ;\mBbbZ{}  \mtimes{}  \mBbbZ{};\mlambda{}a.<a,  n  \mdiv{}  \000Ca>)
By
Latex:
(D  0  THEN  Reduce  0  THEN  Auto)
Home
Index