### Nuprl Lemma : weak-continuity-skolem-truncated

`∀[T:{T:Type| (T ⊆r ℕ) ∧ (↓T)} ]. ∀F:(ℕ ⟶ T) ⟶ ℕ. ⇃(weak-continuity-skolem(T;F))`

Proof

Definitions occuring in Statement :  weak-continuity-skolem: `weak-continuity-skolem(T;F)` quotient: `x,y:A//B[x; y]` nat: `ℕ` subtype_rel: `A ⊆r B` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` squash: `↓T` and: `P ∧ Q` true: `True` set: `{x:A| B[x]} ` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` member: `t ∈ T` subtype_rel: `A ⊆r B` sq-basic-strong-continuity: `sq-basic-strong-continuity(T;F)` sq_exists: `∃x:A [B[x]]` basic-strong-continuity: `basic-strong-continuity(T;F)` prop: `ℙ` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` uimplies: `b supposing a` implies: `P `` Q` guard: `{T}` and: `P ∧ Q`
Lemmas referenced :  Kleene-M_wf subtype_rel_self quotient_wf basic-strong-continuity_wf true_wf equiv_rel_true implies-quotient-true weak-continuity-skolem_wf strong-continuity2-weak-skolem basic-implies-strong-continuity2 istype-nat istype-universe subtype_rel_wf nat_wf squash_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  Error :lambdaFormation_alt,  cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis applyEquality sqequalRule because_Cache Error :lambdaEquality_alt,  Error :inhabitedIsType,  Error :universeIsType,  setElimination rename independent_isectElimination independent_functionElimination Error :functionIsType,  Error :setIsType,  instantiate universeEquality Error :productIsType

Latex:
\mforall{}[T:\{T:Type|  (T  \msubseteq{}r  \mBbbN{})  \mwedge{}  (\mdownarrow{}T)\}  ].  \mforall{}F:(\mBbbN{}  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbN{}.  \00D9(weak-continuity-skolem(T;F))

Date html generated: 2019_06_20-PM-02_51_14
Last ObjectModification: 2019_02_09-PM-11_56_39

Theory : continuity

Home Index