### Nuprl Lemma : basic-implies-strong-continuity2

`∀[T:Type]. ∀[F:(ℕ ⟶ T) ⟶ ℕ].  (basic-strong-continuity(T;F) `` strong-continuity2(T;F))`

Proof

Definitions occuring in Statement :  strong-continuity2: `strong-continuity2(T;F)` basic-strong-continuity: `basic-strong-continuity(T;F)` nat: `ℕ` uall: `∀[x:A]. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` basic-strong-continuity: `basic-strong-continuity(T;F)` member: `t ∈ T` prop: `ℙ` sq_exists: `∃x:A [B[x]]` exists: `∃x:A. B[x]` nat: `ℕ` bool: `𝔹` ifthenelse: `if b then t else f fi ` all: `∀x:A. B[x]` b-union: `A ⋃ B` so_apply: `x[s]` so_lambda: `λ2x.t[x]` cand: `A c∧ B` and: `P ∧ Q` uimplies: `b supposing a` false: `False` not: `¬A` isl: `isl(x)` int?: `int?(x)` subtype_rel: `A ⊆r B` pi2: `snd(t)` tunion: `⋃x:A.B[x]` unit: `Unit` sq_stable: `SqStable(P)` squash: `↓T` top: `Top` satisfiable_int_formula: `satisfiable_int_formula(fmla)` or: `P ∨ Q` decidable: `Dec(P)` ge: `i ≥ j ` guard: `{T}` sq_type: `SQType(T)` has-value: `(a)↓` less_than': `less_than'(a;b)` le: `A ≤ B` true: `True` assert: `↑b` btrue: `tt` bfalse: `ff` strong-continuity2: `strong-continuity2(T;F)` rev_implies: `P `` Q` iff: `P `⇐⇒` Q`
Lemmas referenced :  basic-strong-continuity_wf istype-nat istype-universe int_seg_wf it_wf unit_wf2 product_subtype_base int_subtype_base set_subtype_base ifthenelse_wf bool_wf tunion_subtype_base product-value-type int-value-type istype-int le_wf set-value-type bunion-value-type nat_wf b-union_wf int?_wf btrue_neq_bfalse bfalse_wf btrue_wf istype-sqequal equal-wf-base sq_stable__all sq_stable__equal istype-le int_formula_prop_wf int_formula_prop_eq_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma istype-void int_formula_prop_and_lemma intformeq_wf itermVar_wf itermConstant_wf intformle_wf intformnot_wf intformand_wf full-omega-unsat decidable__le nat_properties subtype_base_sq value-type-has-value subtype_rel_self istype-false int_seg_subtype_nat subtype_rel_function istype-true istype-assert unit_subtype_base union_subtype_base equal-wf-base-T squash_wf iff_weakening_equal true_wf equal_wf mu_wf bool_subtype_base mu-property
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt lambdaFormation_alt sqequalHypSubstitution universeIsType cut introduction extract_by_obid isectElimination thin hypothesisEquality hypothesis functionIsType because_Cache instantiate universeEquality setElimination rename dependent_pairFormation_alt natural_numberEquality lambdaEquality_alt independent_functionElimination dependent_functionElimination equalitySymmetry equalityTransitivity equalityIstype inrEquality_alt inlEquality_alt applyEquality unionElimination independent_pairFormation inhabitedIsType intEquality sqequalRule independent_isectElimination productEquality closedConclusion voidElimination applyLambdaEquality productIsType dependent_set_memberEquality_alt productElimination sqequalBase setIsType unionIsType baseClosed baseApply sqequalIntensionalEquality setEquality unionEquality imageElimination equalityElimination axiomEquality functionIsTypeImplies imageMemberEquality isect_memberEquality_alt int_eqEquality approximateComputation cumulativity isintReduceTrue callbyvalueReduce independent_pairEquality isectIsType dependent_pairEquality_alt

Latex:
\mforall{}[T:Type].  \mforall{}[F:(\mBbbN{}  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbN{}].    (basic-strong-continuity(T;F)  {}\mRightarrow{}  strong-continuity2(T;F))

Date html generated: 2020_05_19-PM-10_04_31
Last ObjectModification: 2020_01_04-PM-08_04_32

Theory : continuity

Home Index