---

Step * 1 1 of Lemma cardinality-le-int_seg

.....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)))
BY
{ (D 0 THEN Reduce 0 THEN Auto') }

1
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
8. a1 : ℕy - x
9. a2 : ℕy - x
10. (g (x + a1)) = (g (x + a2)) ∈ ℕn
⊢ a1 = a2 ∈ ℕy - x

---

Latex:

---

Latex:
.....antecedent..... 
1.  x  :  \mBbbZ{}
2.  y  :  \mBbbZ{}
3.  n  :  \mBbbN{}
4.  f  :  \mBbbN{}n  {}\mrightarrow{}  \{x..y\msupminus{}\}
5.  g  :  \{x..y\msupminus{}\}  {}\mrightarrow{}  \mBbbN{}n
6.  \mforall{}x1:\{x..y\msupminus{}\}.  ((f  (g  x1))  =  x1)
7.  x  <  y
\mvdash{}  Inj(\mBbbN{}y  -  x;\mBbbN{}n;\mlambda{}i.(g  (x  +  i)))


By

---

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

---

Home Index