---

Step * 1 2 2 1 1 1 1 of Lemma unbounded-decidable-nset-infinite


1. d : ℕ ⟶ 𝔹
2. n : ℕ
3. m : ℕ
4. m < n
5. ∀j:ℕ. (m < j ⇒ (↑(d j)) ⇒ (n ≤ j))
6. ↑(d m)
7. (∀[x,y:ℕ].  (x = y ∈ ℕ) supposing ((y ∈ filter(d;[m, n))) and (x ∈ filter(d;[m, n)))))
   ∧ no_repeats(ℕ;filter(d;[m, n)))
   ∧ 0 < ||filter(d;[m, n))|| 
   supposing ||filter(d;[m, n))|| = 1 ∈ ℤ
8. x : ℕ
9. y : ℕ
10. (x ∈ filter(d;[m, n)))
11. (y ∈ filter(d;[m, n)))
⊢ x = y ∈ ℕ
BY
{ (GenListD (-2) THEN GenListD (-1) THEN Auto) }

1
1. d : ℕ ⟶ 𝔹
2. n : ℕ
3. m : ℕ
4. m < n
5. ∀j:ℕ. (m < j ⇒ (↑(d j)) ⇒ (n ≤ j))
6. ↑(d m)
7. (∀[x,y:ℕ].  (x = y ∈ ℕ) supposing ((y ∈ filter(d;[m, n))) and (x ∈ filter(d;[m, n)))))
   ∧ no_repeats(ℕ;filter(d;[m, n)))
   ∧ 0 < ||filter(d;[m, n))|| 
   supposing ||filter(d;[m, n))|| = 1 ∈ ℤ
8. x : ℕ
9. y : ℕ
10. (x ∈ [m, n))
11. ↑(d x)
12. (y ∈ [m, n))
13. ↑(d y)
⊢ x = y ∈ ℕ

---

Latex:

---

Latex:

1.  d  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
2.  n  :  \mBbbN{}
3.  m  :  \mBbbN{}
4.  m  <  n
5.  \mforall{}j:\mBbbN{}.  (m  <  j  {}\mRightarrow{}  (\muparrow{}(d  j))  {}\mRightarrow{}  (n  \mleq{}  j))
6.  \muparrow{}(d  m)
7.  (\mforall{}[x,y:\mBbbN{}].    (x  =  y)  supposing  ((y  \mmember{}  filter(d;[m,  n)))  and  (x  \mmember{}  filter(d;[m,  n)))))
      \mwedge{}  no\_repeats(\mBbbN{};filter(d;[m,  n)))
      \mwedge{}  0  <  ||filter(d;[m,  n))|| 
      supposing  ||filter(d;[m,  n))||  =  1
8.  x  :  \mBbbN{}
9.  y  :  \mBbbN{}
10.  (x  \mmember{}  filter(d;[m,  n)))
11.  (y  \mmember{}  filter(d;[m,  n)))
\mvdash{}  x  =  y


By

---

Latex:
(GenListD  (-2)  THEN  GenListD  (-1)  THEN  Auto)

---

Home Index