---

Step * 1 of Lemma cardinality-le-int_seg


1. x : ℤ
2. y : ℤ
3. n : ℕ
4. f : ℕn ⟶ {x..y-}
5. Surj(ℕn;{x..y-};f)
6. x < y
⊢ (y - x) ≤ n
BY
{ (((RWO "surject-inverse" (-2) THENA Auto) THEN ExRepD)
   THEN InstLemma `pigeon-hole` [⌜y - x⌝;⌜n⌝;⌜λi.(g (x + i))⌝]⋅
   THEN Auto') }

1
.....antecedent..... 
1. x : ℤ
2. y : ℤ
3. n : ℕ
4. f : ℕn ⟶ {x..y-}
5. g : {x..y-} ⟶ ℕn
6. ∀x1:{x..y-}. ((f (g x1)) = x1 ∈ {x..y-})
7. x < y
⊢ Inj(ℕy - x;ℕn;λi.(g (x + i)))

---

Latex:

---

Latex:

1.  x  :  \mBbbZ{}
2.  y  :  \mBbbZ{}
3.  n  :  \mBbbN{}
4.  f  :  \mBbbN{}n  {}\mrightarrow{}  \{x..y\msupminus{}\}
5.  Surj(\mBbbN{}n;\{x..y\msupminus{}\};f)
6.  x  <  y
\mvdash{}  (y  -  x)  \mleq{}  n


By

---

Latex:
(((RWO  "surject-inverse"  (-2)  THENA  Auto)  THEN  ExRepD)
  THEN  InstLemma  `pigeon-hole`  [\mkleeneopen{}y  -  x\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}\mlambda{}i.(g  (x  +  i))\mkleeneclose{}]\mcdot{}
  THEN  Auto')

---

Home Index