Nuprl Lemma : k-1-continuous_wf

[k:ℕ]. ∀[F:(ℕk ⟶ Type) ⟶ Type].  (k-1-continuous{i:l}(k;T.F[T]) ∈ ℙ')


Proof




Definitions occuring in Statement :  k-1-continuous: k-1-continuous{i:l}(k;T.F[T]) int_seg: {i..j-} nat: uall: [x:A]. B[x] prop: so_apply: x[s] member: t ∈ T function: x:A ⟶ B[x] natural_number: $n universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T k-1-continuous: k-1-continuous{i:l}(k;T.F[T]) subtype_rel: A ⊆B nat: so_lambda: λ2x.t[x] implies:  Q all: x:A. B[x] decidable: Dec(P) or: P ∨ Q iff: ⇐⇒ Q and: P ∧ Q not: ¬A rev_implies:  Q false: False prop: uiff: uiff(P;Q) uimplies: supposing a sq_stable: SqStable(P) squash: T subtract: m top: Top le: A ≤ B less_than': less_than'(a;b) true: True so_apply: x[s]
Lemmas referenced :  uall_wf nat_wf int_seg_wf all_wf k-subtype_wf decidable__le false_wf not-le-2 sq_stable__le condition-implies-le minus-add minus-one-mul zero-add minus-one-mul-top add-associates add-swap add-commutes add_functionality_wrt_le add-zero le-add-cancel le_wf subtype_rel_wf k-intersection_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule thin instantiate extract_by_obid sqequalHypSubstitution isectElimination functionEquality hypothesis applyEquality lambdaEquality cumulativity hypothesisEquality universeEquality natural_numberEquality setElimination rename because_Cache functionExtensionality dependent_set_memberEquality addEquality dependent_functionElimination unionElimination independent_pairFormation lambdaFormation voidElimination productElimination independent_functionElimination independent_isectElimination imageMemberEquality baseClosed imageElimination isect_memberEquality voidEquality intEquality minusEquality isectEquality axiomEquality equalityTransitivity equalitySymmetry

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[F:(\mBbbN{}k  {}\mrightarrow{}  Type)  {}\mrightarrow{}  Type].    (k-1-continuous\{i:l\}(k;T.F[T])  \mmember{}  \mBbbP{}')



Date html generated: 2018_05_21-PM-00_09_26
Last ObjectModification: 2017_10_18-PM-02_34_26

Theory : co-recursion


Home Index