### Nuprl Lemma : strong-continuous-list

`∀[F:Type ⟶ Type]. Continuous+(T.F[T] List) supposing Continuous+(T.F[T])`

Proof

Definitions occuring in Statement :  list: `T List` strong-type-continuous: `Continuous+(T.F[T])` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s]` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  so_apply: `x[s]` uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` strong-type-continuous: `Continuous+(T.F[T])` ext-eq: `A ≡ B` and: `P ∧ Q` subtype_rel: `A ⊆r B` prop: `ℙ` so_lambda: `λ2x.t[x]` all: `∀x:A. B[x]` nat: `ℕ` le: `A ≤ B` less_than': `less_than'(a;b)` false: `False` not: `¬A` implies: `P `` Q` int_seg: `{i..j-}` sq_stable: `SqStable(P)` lelt: `i ≤ j < k` squash: `↓T` or: `P ∨ Q` decidable: `Dec(P)` top: `Top` exists: `∃x:A. B[x]` satisfiable_int_formula: Error :satisfiable_int_formula,  ge: `i ≥ j ` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` uiff: `uiff(P;Q)` subtract: `n - m` true: `True` gt: `i > j`
Lemmas referenced :  nat_wf list_wf strong-type-continuous_wf false_wf le_wf nat_properties length_wf_nat equal_wf select_wf sq_stable__le int_seg_wf length_wf Error :int_term_value_subtract_lemma,  Error :int_formula_prop_not_lemma,  Error :itermSubtract_wf,  Error :intformnot_wf,  subtract_wf decidable__le less_than_wf ge_wf Error :int_formula_prop_wf,  Error :int_formula_prop_less_lemma,  Error :int_term_value_var_lemma,  Error :int_term_value_constant_lemma,  Error :int_formula_prop_le_lemma,  Error :int_formula_prop_and_lemma,  Error :intformless_wf,  Error :itermVar_wf,  Error :itermConstant_wf,  Error :intformle_wf,  Error :intformand_wf,  Error :satisfiable-full-omega-tt,  first0 subtype_rel_list top_wf nil_wf decidable__lt firstn_decomp le_weakening2 append_wf cons_wf not-le-2 less-iff-le condition-implies-le minus-one-mul zero-add minus-one-mul-top minus-add minus-minus add-associates add-swap add-commutes add_functionality_wrt_le add-zero le-add-cancel lelt_wf firstn_all not-gt-2 not-lt-2 le-add-cancel2 le_reflexive
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut independent_pairFormation lambdaEquality isectEquality extract_by_obid hypothesis sqequalHypSubstitution isectElimination thin applyEquality functionExtensionality hypothesisEquality universeEquality isect_memberEquality productElimination independent_pairEquality axiomEquality functionEquality cumulativity because_Cache equalityTransitivity equalitySymmetry lambdaFormation dependent_set_memberEquality natural_numberEquality dependent_functionElimination independent_functionElimination setElimination rename independent_isectElimination imageMemberEquality baseClosed imageElimination unionElimination computeAll voidEquality voidElimination intEquality int_eqEquality dependent_pairFormation intWeakElimination addEquality minusEquality comment

Latex:
\mforall{}[F:Type  {}\mrightarrow{}  Type].  Continuous+(T.F[T]  List)  supposing  Continuous+(T.F[T])

Date html generated: 2018_05_21-PM-00_20_45
Last ObjectModification: 2017_10_18-PM-00_43_48

Theory : list_0

Home Index