### Nuprl Lemma : strong-continuity2-implies-weak-skolem

`∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ⇃(∃M:(ℕ ⟶ ℕ) ⟶ ℕ. ∀f,g:ℕ ⟶ ℕ.  ((f = g ∈ (ℕM f ⟶ ℕ)) `` ((F f) = (F g) ∈ ℕ)))`

Proof

Definitions occuring in Statement :  quotient: `x,y:A//B[x; y]` int_seg: `{i..j-}` nat: `ℕ` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` true: `True` apply: `f a` function: `x:A ⟶ B[x]` natural_number: `\$n` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` strong-continuity2: `strong-continuity2(T;F)` weak-continuity-skolem: `weak-continuity-skolem(T;F)` uall: `∀[x:A]. B[x]` implies: `P `` Q` prop: `ℙ` guard: `{T}`
Lemmas referenced :  strong-continuity2-no-inner-squash implies-quotient-true strong-continuity2_wf nat_wf weak-continuity-skolem_wf strong-continuity2-weak-skolem
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality hypothesis isectElimination functionExtensionality applyEquality functionEquality independent_functionElimination because_Cache

Latex:
\mforall{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  \00D9(\mexists{}M:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  \mforall{}f,g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.    ((f  =  g)  {}\mRightarrow{}  ((F  f)  =  (F  g))))

Date html generated: 2016_12_12-AM-09_23_24
Last ObjectModification: 2016_11_22-PM-00_07_27

Theory : continuity

Home Index