---

Step * 1 of Lemma two-factorizations-no-repeats


1. n : ℕ
⊢ no_repeats(ℤ × ℤ;map(λa.<a, n ÷ a>;filter(λa.(n rem a =z 0);[1, n + 1))))
BY
{ (Using [`T', ⌜{x:ℤ| (1 ≤ x) ∧ x < n + 1} ⌝] (BLemma `no_repeats_map`)⋅ THENA Auto) }

1
1. n : ℕ
⊢ no_repeats({x:ℤ| (1 ≤ x) ∧ x < n + 1} ;filter(λa.(n rem a =z 0);[1, n + 1)))

2
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>)

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
\mvdash{}  no\_repeats(\mBbbZ{}  \mtimes{}  \mBbbZ{};map(\mlambda{}a.<a,  n  \mdiv{}  a>filter(\mlambda{}a.(n  rem  a  =\msubz{}  0);[1,  n  +  1))))


By

---

Latex:
(Using  [`T',  \mkleeneopen{}\{x:\mBbbZ{}|  (1  \mleq{}  x)  \mwedge{}  x  <  n  +  1\}  \mkleeneclose{}]  (BLemma  `no\_repeats\_map`)\mcdot{}  THENA  Auto)

---

Home Index