Step
*
2
1
1
of Lemma
mu-bound-property
1. b : ℕ
2. f : ℕb ⟶ 𝔹
3. ∃n:ℕb. (↑(f n))
4. mu(f) ∈ ℕb
5. (↑(f mu(f))) ∧ (∀[i:ℕmu(f)]. (¬↑(f i)))
⊢ (↑(f mu(f))) ∧ (∀[i:ℕb]. ¬↑(f i) supposing i < mu(f))
BY
{ Auto }
Latex:
Latex:
1. b : \mBbbN{}
2. f : \mBbbN{}b {}\mrightarrow{} \mBbbB{}
3. \mexists{}n:\mBbbN{}b. (\muparrow{}(f n))
4. mu(f) \mmember{} \mBbbN{}b
5. (\muparrow{}(f mu(f))) \mwedge{} (\mforall{}[i:\mBbbN{}mu(f)]. (\mneg{}\muparrow{}(f i)))
\mvdash{} (\muparrow{}(f mu(f))) \mwedge{} (\mforall{}[i:\mBbbN{}b]. \mneg{}\muparrow{}(f i) supposing i < mu(f))
By
Latex:
Auto
Home
Index