Step
*
1
of Lemma
mu-ge-bound
.....assertion.....
∀d:ℕ. ∀[n,m:ℤ]. (((m - n) ≤ d)
⇒ (∀[f:{n..m-} ⟶ 𝔹]. mu-ge(f;n) ∈ {n..m-} supposing ∃k:{n..m-}. (↑(f k))))
BY
{ (InductionOnNat THEN (UnivCD THENA Auto) THEN ExRepD) }
1
1. d : ℤ
2. n : ℤ
3. m : ℤ
4. (m - n) ≤ 0
5. f : {n..m-} ⟶ 𝔹
6. k : {n..m-}
7. ↑(f k)
⊢ mu-ge(f;n) ∈ {n..m-}
2
1. d : ℤ
2. 0 < d
3. ∀[n,m:ℤ]. (((m - n) ≤ (d - 1))
⇒ (∀[f:{n..m-} ⟶ 𝔹]. mu-ge(f;n) ∈ {n..m-} supposing ∃k:{n..m-}. (↑(f k))))
4. n : ℤ
5. m : ℤ
6. (m - n) ≤ d
7. f : {n..m-} ⟶ 𝔹
8. k : {n..m-}
9. ↑(f k)
⊢ mu-ge(f;n) ∈ {n..m-}
Latex:
Latex:
.....assertion.....
\mforall{}d:\mBbbN{}
\mforall{}[n,m:\mBbbZ{}].
(((m - n) \mleq{} d) {}\mRightarrow{} (\mforall{}[f:\{n..m\msupminus{}\} {}\mrightarrow{} \mBbbB{}]. mu-ge(f;n) \mmember{} \{n..m\msupminus{}\} supposing \mexists{}k:\{n..m\msupminus{}\}. (\muparrow{}(f k))))
By
Latex:
(InductionOnNat THEN (UnivCD THENA Auto) THEN ExRepD)
Home
Index