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