---

Step * 1 of Lemma rinv_wf

.....assertion..... 
1. x : ℝ
2. ∃n:ℕ+. 4 < |x n|
⊢ mu-ge(λn.eval k = x n in 4 <z |k|;1) = mu-ge(λn.4 <z |x n|;1) ∈ {1...}
BY
{ EqCD }

1
.....subterm..... T:t
2:n
1. x : ℝ
2. ∃n:ℕ+. 4 < |x n|
⊢ 1 = 1 ∈ ℤ

2
.....subterm..... T:t
1:n
1. x : ℝ
2. ∃n:ℕ+. 4 < |x n|
⊢ (λn.eval k = x n in 4 <z |k|) = (λn.4 <z |x n|) ∈ ({1...} ⟶ 𝔹)

3
.....antecedent..... 
1. x : ℝ
2. ∃n:ℕ+. 4 < |x n|
⊢ ∃m:{1...}. (↑((λn.eval k = x n in 4 <z |k|) m))

---

Latex:

---

Latex:
.....assertion..... 
1.  x  :  \mBbbR{}
2.  \mexists{}n:\mBbbN{}\msupplus{}.  4  <  |x  n|
\mvdash{}  mu-ge(\mlambda{}n.eval  k  =  x  n  in  4  <z  |k|;1)  =  mu-ge(\mlambda{}n.4  <z  |x  n|;1)


By

---

Latex:
EqCD

---

Home Index