---

Step * 2 of Lemma uniform-continuity-pi-search_wf


1. n : ℕ
2. G : ∀m:ℕn. (Top + Top)
3. x : ℕ
4. ¬x < n
⊢ uniform-continuity-pi-search(
  G;
  n;x) ∈ ℕ
BY
{ (RecUnfold `uniform-continuity-pi-search` 0 THEN AutoSplit) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  G  :  \mforall{}m:\mBbbN{}n.  (Top  +  Top)
3.  x  :  \mBbbN{}
4.  \mneg{}x  <  n
\mvdash{}  uniform-continuity-pi-search(
    G;
    n;x)  \mmember{}  \mBbbN{}


By

---

Latex:
(RecUnfold  `uniform-continuity-pi-search`  0  THEN  AutoSplit)

---

Home Index