---

Step * 1 2 2 1 1 1 2 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,y:ℕ].  (x = y ∈ ℕ) supposing ((y ∈ filter(d;[m, n))) and (x ∈ filter(d;[m, n))))
⊢ no_repeats(ℕ;filter(d;[m, n)))
BY
{ ((BLemma `no_repeats_filter` THEN Auto) THEN InstLemma `no_repeats_from-upto` [⌜m⌝;⌜n⌝]⋅ THEN Auto) }

---

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.  \mforall{}[x,y:\mBbbN{}].    (x  =  y)  supposing  ((y  \mmember{}  filter(d;[m,  n)))  and  (x  \mmember{}  filter(d;[m,  n))))
\mvdash{}  no\_repeats(\mBbbN{};filter(d;[m,  n)))


By

---

Latex:
((BLemma  `no\_repeats\_filter`  THEN  Auto)  THEN  InstLemma  `no\_repeats\_from-upto`  [\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index