### Nuprl Lemma : strong-continuity3-implies-4

`∀[T:Type]. ∀F:(ℕ ⟶ T) ⟶ ℕ. (strong-continuity3(T;F) `` strong-continuity4(T;F))`

Proof

Definitions occuring in Statement :  strong-continuity4: `strong-continuity4(T;F)` strong-continuity3: `strong-continuity3(T;F)` nat: `ℕ` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` strong-continuity3: `strong-continuity3(T;F)` exists: `∃x:A. B[x]` strong-continuity4: `strong-continuity4(T;F)` member: `t ∈ T` prop: `ℙ` nat: `ℕ` so_lambda: `λ2x.t[x]` and: `P ∧ Q` int_seg: `{i..j-}` lelt: `i ≤ j < k` le: `A ≤ B` less_than: `a < b` squash: `↓T` ge: `i ≥ j ` decidable: `Dec(P)` or: `P ∨ Q` uimplies: `b supposing a` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` false: `False` subtype_rel: `A ⊆r B` less_than': `less_than'(a;b)` sq_stable: `SqStable(P)` guard: `{T}` isl: `isl(x)` outl: `outl(x)` so_apply: `x[s]` pi1: `fst(t)` bfalse: `ff` top: `Top` btrue: `tt` ifthenelse: `if b then t else f fi ` assert: `↑b` uiff: `uiff(P;Q)` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` true: `True` sq_type: `SQType(T)` cand: `A c∧ B`
Lemmas referenced :  strong-continuity3_wf istype-nat istype-universe decidable__exists_int_seg assert_wf int_seg_properties nat_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf istype-int int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf istype-le subtype_rel_function int_seg_wf int_seg_subtype istype-false sq_stable__le le_weakening2 subtype_rel_self btrue_wf bfalse_wf less_than_wf assert_elim btrue_neq_bfalse decidable__and2 istype-assert decidable__assert decidable__lt unit_wf2 union_subtype_base set_subtype_base lelt_wf int_subtype_base unit_subtype_base nat_wf int_seg_subtype_nat subtype_rel_union it_wf le_wf true_wf istype-void imax_wf add_nat_wf imax_nat add-is-int-iff itermAdd_wf intformeq_wf int_term_value_add_lemma int_formula_prop_eq_lemma false_wf pi1_wf decidable_wf iff_weakening_equal equal_wf subtype_base_sq squash_wf bool_subtype_base bool_wf isl_wf int_formula_prop_less_lemma intformless_wf imax_ub
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt lambdaFormation_alt sqequalHypSubstitution productElimination thin universeIsType cut introduction extract_by_obid isectElimination hypothesisEquality hypothesis functionIsType because_Cache instantiate universeEquality dependent_functionElimination natural_numberEquality setElimination rename sqequalRule lambdaEquality_alt productEquality applyEquality dependent_set_memberEquality_alt imageElimination unionElimination independent_isectElimination approximateComputation independent_functionElimination dependent_pairFormation_alt int_eqEquality Error :memTop,  independent_pairFormation voidElimination imageMemberEquality baseClosed inhabitedIsType equalityIstype equalityTransitivity equalitySymmetry productIsType applyLambdaEquality isect_memberEquality_alt unionIsType intEquality inlEquality_alt sqequalBase equalityIsType1 inrEquality_alt functionExtensionality addEquality pointwiseFunctionality promote_hyp baseApply closedConclusion dependent_pairEquality_alt functionEquality unionEquality cumulativity inlFormation_alt inrFormation_alt

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

Date html generated: 2020_05_19-PM-10_04_36
Last ObjectModification: 2020_01_04-PM-08_04_04

Theory : continuity

Home Index