---

Step * 1 of Lemma permutation-when-no_repeats


1. [T] : Type
2. sa : T List
3. sb : T List
4. ∀x:T. ((x ∈ sa) ⇐⇒ (x ∈ sb))
5. no_repeats(T;sb)
6. no_repeats(T;sa)
7. ∀i:ℕ||sa||. ∃j:ℕ||sb||. (sa[i] = sb[j] ∈ T)
⊢ permutation(T;sb;sa)
BY
{ (Skolemize (-1) `f' THEN Auto) }

1
1. [T] : Type
2. sa : T List
3. sb : T List
4. ∀x:T. ((x ∈ sa) ⇐⇒ (x ∈ sb))
5. no_repeats(T;sb)
6. no_repeats(T;sa)
7. ∀i:ℕ||sa||. ∃j:ℕ||sb||. (sa[i] = sb[j] ∈ T)
8. f : i:ℕ||sa|| ⟶ ℕ||sb||
9. ∀i:ℕ||sa||. (sa[i] = sb[f i] ∈ T)
⊢ permutation(T;sb;sa)

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  sa  :  T  List
3.  sb  :  T  List
4.  \mforall{}x:T.  ((x  \mmember{}  sa)  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  sb))
5.  no\_repeats(T;sb)
6.  no\_repeats(T;sa)
7.  \mforall{}i:\mBbbN{}||sa||.  \mexists{}j:\mBbbN{}||sb||.  (sa[i]  =  sb[j])
\mvdash{}  permutation(T;sb;sa)


By

---

Latex:
(Skolemize  (-1)  `f'  THEN  Auto)

---

Home Index