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