Nuprl Lemma : weak-continuity-principle-real-ext
∀x:ℝ. ∀F:ℝ ⟶ 𝔹. ∀G:n:ℕ+ ⟶ {y:ℝ| x = y ∈ (ℕ+n ⟶ ℤ)} . (∃n:ℕ+ [F x = F (G n)])
Proof
Definitions occuring in Statement :
real: ℝ,
int_seg: {i..j-},
nat_plus: ℕ+,
bool: 𝔹,
all: ∀x:A. B[x],
sq_exists: ∃x:A [B[x]],
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions unfolded in proof :
member: t ∈ T,
weak-continuity-principle-real,
WCPR: WCPR(F;x;G)
Lemmas referenced :
weak-continuity-principle-real
Rules used in proof :
introduction,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
instantiate,
extract_by_obid,
hypothesis,
sqequalRule,
thin,
sqequalHypSubstitution,
equalityTransitivity,
equalitySymmetry
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)])
Date html generated:
2018_05_22-PM-02_16_17
Last ObjectModification:
2018_05_20-PM-02_46_27
Theory : reals
Home
Index