Nuprl Lemma : strong-continuity3_functionality

`∀[T,S:Type].  ∀e:T ~ S. ∀F:(ℕ ⟶ S) ⟶ ℕ.  (strong-continuity3(T;λf.(F ((fst(e)) o f))) `` strong-continuity3(S;F))`

Proof

Definitions occuring in Statement :  strong-continuity3: `strong-continuity3(T;F)` equipollent: `A ~ B` compose: `f o g` nat: `ℕ` uall: `∀[x:A]. B[x]` pi1: `fst(t)` all: `∀x:A. B[x]` implies: `P `` Q` apply: `f a` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  prop: `ℙ` pi1: `fst(t)` member: `t ∈ T` and: `P ∧ Q` biject: `Bij(A;B;f)` exists: `∃x:A. B[x]` equipollent: `A ~ B` implies: `P `` Q` all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]`
Lemmas referenced :  equipollent_wf compose_wf nat_wf strong-continuity3_wf strong-continuity3_functionality_surject
Rules used in proof :  universeEquality because_Cache functionEquality functionExtensionality applyEquality lambdaEquality cumulativity sqequalRule hypothesis independent_functionElimination dependent_functionElimination hypothesisEquality isectElimination extract_by_obid introduction cut thin productElimination sqequalHypSubstitution lambdaFormation isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[T,S:Type].
\mforall{}e:T  \msim{}  S.  \mforall{}F:(\mBbbN{}  {}\mrightarrow{}  S)  {}\mrightarrow{}  \mBbbN{}.
(strong-continuity3(T;\mlambda{}f.(F  ((fst(e))  o  f)))  {}\mRightarrow{}  strong-continuity3(S;F))

Date html generated: 2017_09_29-PM-06_05_12
Last ObjectModification: 2017_09_04-AM-09_02_31

Theory : continuity

Home Index