---

Step * 1 1 of Lemma equipollent_interval


1. a : ℤ@i
2. b : ℤ@i
⊢ Bij({a..b-};ℕb - a;λn.(n - a))
BY
{ (RepeatFor 2 (D 0) THEN Reduce 0 THEN Auto') }

1
1. a : ℤ@i
2. b : ℤ@i
3. b@0 : ℕb - a@i
⊢ ∃a@0:{a..b-}. ((a@0 - a) = b@0 ∈ ℕb - a)

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}@i
2.  b  :  \mBbbZ{}@i
\mvdash{}  Bij(\{a..b\msupminus{}\};\mBbbN{}b  -  a;\mlambda{}n.(n  -  a))


By

---

Latex:
(RepeatFor  2  (D  0)  THEN  Reduce  0  THEN  Auto')

---

Home Index