---

Step * 1 1 1 of Lemma cardinality-le-int_seg


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
BY
{ (Assert (f (g (x + a1))) = (f (g (x + a2))) ∈ {x..y-} BY
         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
11. (f (g (x + a1))) = (f (g (x + a2))) ∈ {x..y-}
⊢ a1 = a2 ∈ ℕy - x

---

Latex:

---

Latex:

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
8.  a1  :  \mBbbN{}y  -  x
9.  a2  :  \mBbbN{}y  -  x
10.  (g  (x  +  a1))  =  (g  (x  +  a2))
\mvdash{}  a1  =  a2


By

---

Latex:
(Assert  (f  (g  (x  +  a1)))  =  (f  (g  (x  +  a2)))  BY
              Auto')

---

Home Index