---

Step * of Lemma int_seg-cardinality-le

∀i,j:ℤ.  |{i..j-}| ≤ if i ≤z j then j - i else 0 fi 
BY
{ (Auto THEN UnfoldTopAb 0 THEN (SplitOnConclITE THENA Auto)) }

1
.....truecase..... 
1. i : ℤ
2. j : ℤ
3. i ≤ j
⊢ ∃f:ℕj - i ⟶ {i..j-}. Surj(ℕj - i;{i..j-};f)

2
.....falsecase..... 
1. i : ℤ
2. j : ℤ
3. j < i
⊢ ∃f:ℕ0 ⟶ {i..j-}. Surj(ℕ0;{i..j-};f)

---

Latex:

---

Latex:
\mforall{}i,j:\mBbbZ{}.    |\{i..j\msupminus{}\}|  \mleq{}  if  i  \mleq{}z  j  then  j  -  i  else  0  fi 


By

---

Latex:
(Auto  THEN  UnfoldTopAb  0  THEN  (SplitOnConclITE  THENA  Auto))

---

Home Index