---

Step * 1 of Lemma equipollent_interval


1. a : ℤ@i
2. b : ℤ@i
⊢ ∃f:{a..b-} ⟶ ℕb - a. Bij({a..b-};ℕb - a;f)
BY
{ ((InstConcl [⌜λn.(n - a)⌝])⋅ THENA Auto') }

1
1. a : ℤ@i
2. b : ℤ@i
⊢ Bij({a..b-};ℕb - a;λn.(n - a))

---

Latex:

---

Latex:

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


By

---

Latex:
((InstConcl  [\mkleeneopen{}\mlambda{}n.(n  -  a)\mkleeneclose{}])\mcdot{}  THENA  Auto')

---

Home Index