Nuprl Lemma : weak-continuity-principle-real-double

x:ℝ. ∀F,H:ℝ ⟶ 𝔹. ∀G:n:ℕ+ ⟶ {y:ℝy ∈ (ℕ+n ⟶ ℤ)} .  (∃n:{ℕ+(F (G n) ∧ (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]} and: P ∧ Q set: {x:A| B[x]}  apply: a function: x:A ⟶ B[x] natural_number: $n int: equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T prop: uall: [x:A]. B[x] nat_plus: + real: subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s] uimplies: supposing a le: A ≤ B and: P ∧ Q less_than': less_than'(a;b) false: False not: ¬A implies:  Q less_than: a < b squash: T true: True sq_exists: x:{A| B[x]} cand: c∧ B guard: {T} iff: ⇐⇒ Q
Lemmas referenced :  nat_plus_wf real_wf equal_wf int_seg_wf subtype_rel_dep_function int_seg_subtype_nat_plus false_wf subtype_rel_self bool_wf WCPD_wf regularize-k-regular less_than_wf regularize_wf regular-int-seq_wf subtype_rel_sets set_wf squash_wf true_wf regularize-real iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation functionEquality cut introduction extract_by_obid hypothesis setEquality sqequalHypSubstitution isectElimination thin natural_numberEquality setElimination rename because_Cache intEquality hypothesisEquality applyEquality sqequalRule lambdaEquality independent_isectElimination independent_pairFormation dependent_functionElimination functionExtensionality dependent_set_memberEquality imageMemberEquality baseClosed productEquality equalityTransitivity equalitySymmetry independent_functionElimination dependent_set_memberFormation productElimination equalityUniverse levelHypothesis imageElimination universeEquality

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



Date html generated: 2017_10_03-AM-09_09_22
Last ObjectModification: 2017_09_12-PM-02_20_05

Theory : reals


Home Index