---

Step * of Lemma cardinality-le-int_seg

∀[x,y:ℤ]. ∀[n:ℕ].  (y - x) ≤ n supposing |{x..y-}| ≤ n
BY
{ (Auto THEN D -1 THEN Decide x < y THEN Auto') }

1
1. x : ℤ
2. y : ℤ
3. n : ℕ
4. f : ℕn ⟶ {x..y-}
5. Surj(ℕn;{x..y-};f)
6. x < y
⊢ (y - x) ≤ n

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbZ{}].  \mforall{}[n:\mBbbN{}].    (y  -  x)  \mleq{}  n  supposing  |\{x..y\msupminus{}\}|  \mleq{}  n


By

---

Latex:
(Auto  THEN  D  -1  THEN  Decide  x  <  y  THEN  Auto')

---

Home Index