---

Step * of Lemma strict-sorted

∀[T:Type]. ∀[as:T List]. uiff(sorted(as) ∧ no_repeats(T;as);∀[i:ℕ||as||]. ∀[j:ℕi].  as[j] < as[i]) supposing T ⊆r ℤ
BY
{ Auto }

1
1. T : Type
2. T ⊆r ℤ
3. as : T List
4. sorted(as)
5. no_repeats(T;as)
6. i : ℕ||as||
7. j : ℕi
⊢ as[j] < as[i]

2
1. T : Type
2. T ⊆r ℤ
3. as : T List
4. ∀[i:ℕ||as||]. ∀[j:ℕi].  as[j] < as[i]
⊢ sorted(as)

3
1. T : Type
2. T ⊆r ℤ
3. as : T List
4. ∀[i:ℕ||as||]. ∀[j:ℕi].  as[j] < as[i]
⊢ no_repeats(T;as)

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}[as:T  List].  uiff(sorted(as)  \mwedge{}  no\_repeats(T;as);\mforall{}[i:\mBbbN{}||as||].  \mforall{}[j:\mBbbN{}i].    as[j]  <  as[i]) 
    supposing  T  \msubseteq{}r  \mBbbZ{}


By

---

Latex:
Auto

---

Home Index