---

Step * of Lemma weak-continuity-principle-real-ext

∀x:ℝ. ∀F:ℝ ⟶ 𝔹. ∀G:n:ℕ+ ⟶ {y:ℝ| x = y ∈ (ℕ+n ⟶ ℤ)} .  (∃n:ℕ+ [F x = F (G n)])
BY
{ Extract of Obid: weak-continuity-principle-real
  not unfolding  WCP  regularize
  finishing with xxx(Fold `WCPR` 0 THEN Auto)xxx
  normalizes to:
  
  λx,F,G. WCPR(F;x;G) }

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}.  \mforall{}F:\mBbbR{}  {}\mrightarrow{}  \mBbbB{}.  \mforall{}G:n:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \{y:\mBbbR{}|  x  =  y\}  .    (\mexists{}n:\mBbbN{}\msupplus{}  [F  x  =  F  (G  n)])


By

---

Latex:
Extract  of  Obid:  weak-continuity-principle-real
not  unfolding    WCP    regularize
finishing  with  xxx(Fold  `WCPR`  0  THEN  Auto)xxx
normalizes  to:

\mlambda{}x,F,G.  WCPR(F;x;G)

---

Home Index