---

Step * of Lemma equipollent_interval

∀a,b:ℤ.  {a..b-} ~ ℕb - a
BY
{ (Auto THEN Unfold `equipollent` 0) }

1
1. a : ℤ@i
2. b : ℤ@i
⊢ ∃f:{a..b-} ⟶ ℕb - a. Bij({a..b-};ℕb - a;f)

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbZ{}.    \{a..b\msupminus{}\}  \msim{}  \mBbbN{}b  -  a


By

---

Latex:
(Auto  THEN  Unfold  `equipollent`  0)

---

Home Index