Nuprl Lemma : unsquashed-weak-continuity-false2

¬(∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ∀a:ℕ ⟶ ℕ.  ∃n:ℕ. ∀b:ℕ ⟶ ℕ((∀i:ℕn. ((a i) (b i) ∈ ℕ))  ((F a) (F b) ∈ ℕ)))


Proof




Definitions occuring in Statement :  int_seg: {i..j-} nat: all: x:A. B[x] exists: x:A. B[x] not: ¬A implies:  Q apply: a function: x:A ⟶ B[x] natural_number: $n equal: t ∈ T
Definitions unfolded in proof :  not: ¬A implies:  Q unsquashed-WCP: unsquashed-WCP all: x:A. B[x] member: t ∈ T exists: x:A. B[x] prop: uall: [x:A]. B[x] so_lambda: λ2x.t[x] subtype_rel: A ⊆B uimplies: supposing a le: A ≤ B and: P ∧ Q less_than': less_than'(a;b) false: False so_apply: x[s] nat: pi1: fst(t)
Lemmas referenced :  unsquashed-weak-continuity-false all_wf nat_wf int_seg_wf equal_wf int_seg_subtype_nat false_wf exists_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution independent_functionElimination thin hypothesis dependent_functionElimination hypothesisEquality promote_hyp productElimination dependent_pairFormation isectElimination functionEquality because_Cache sqequalRule lambdaEquality natural_numberEquality applyEquality functionExtensionality independent_isectElimination independent_pairFormation voidElimination setElimination rename equalityTransitivity equalitySymmetry

Latex:
\mneg{}(\mforall{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  \mforall{}a:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.    \mexists{}n:\mBbbN{}.  \mforall{}b:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((\mforall{}i:\mBbbN{}n.  ((a  i)  =  (b  i)))  {}\mRightarrow{}  ((F  a)  =  (F  b))))



Date html generated: 2017_04_17-AM-09_41_08
Last ObjectModification: 2017_02_27-PM-05_36_00

Theory : fan-theorem


Home Index