Nuprl Lemma : seq-cont_wf

[T:Type]. ∀[F:(ℕ ⟶ T) ⟶ ℕ].  (seq-cont(T;F) ∈ ℙ)


Proof




Definitions occuring in Statement :  seq-cont: seq-cont(T;F) nat: uall: [x:A]. B[x] prop: member: t ∈ T function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  exists: x:A. B[x] all: x:A. B[x] not: ¬A false: False less_than': less_than'(a;b) and: P ∧ Q le: A ≤ B uimplies: supposing a so_apply: x[s] subtype_rel: A ⊆B nat: prop: implies:  Q so_lambda: λ2x.t[x] seq-cont: seq-cont(T;F) member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  false_wf int_seg_subtype_nat subtype_rel_dep_function int_upper_subtype_nat int_seg_wf equal_wf int_upper_wf exists_wf nat_wf all_wf
Rules used in proof :  universeEquality isect_memberEquality equalitySymmetry equalityTransitivity axiomEquality lambdaFormation independent_pairFormation independent_isectElimination functionExtensionality applyEquality natural_numberEquality rename setElimination because_Cache lambdaEquality hypothesisEquality cumulativity hypothesis functionEquality thin isectElimination sqequalHypSubstitution extract_by_obid sqequalRule cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[T:Type].  \mforall{}[F:(\mBbbN{}  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbN{}].    (seq-cont(T;F)  \mmember{}  \mBbbP{})



Date html generated: 2017_09_29-PM-06_05_45
Last ObjectModification: 2017_07_19-AM-10_22_51

Theory : continuity


Home Index