Nuprl Lemma : unary-almost-full-has-strict-inc

A:ℕ ⟶ ℙ((∀s:StrictInc. ⇃(∃n:ℕA[s n]))  ⇃(∃s:StrictInc. ∀n:ℕA[s n]))


Proof




Definitions occuring in Statement :  strict-inc: StrictInc quotient: x,y:A//B[x; y] nat: prop: so_apply: x[s] all: x:A. B[x] exists: x:A. B[x] implies:  Q true: True apply: a function: x:A ⟶ B[x]
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q member: t ∈ T uall: [x:A]. B[x] exists: x:A. B[x] so_apply: x[s] strict-inc: StrictInc subtype_rel: A ⊆B so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] uimplies: supposing a prop: nat: ge: i ≥  decidable: Dec(P) or: P ∨ Q not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) false: False top: Top and: P ∧ Q int_seg: {i..j-} lelt: i ≤ j < k le: A ≤ B less_than: a < b squash: T guard: {T} cand: c∧ B bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) ifthenelse: if then else fi  bfalse: ff sq_type: SQType(T) bnot: ¬bb assert: b rev_implies:  Q iff: ⇐⇒ Q subtract: m true: True so_lambda: λ2x.t[x]
Lemmas referenced :  strict-inc_wf quotient_wf nat_wf true_wf istype-nat equiv_rel_true nat_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermAdd_wf itermVar_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_add_lemma int_term_value_var_lemma int_formula_prop_wf istype-le int_seg_properties decidable__lt intformless_wf int_formula_prop_less_lemma int_seg_wf istype-less_than implies-quotient-true less_than_wf subtype_rel_self axiom-choice-00-quot implies-strict-inc primrec_wf primrec-unroll lt_int_wf eqtt_to_assert assert_of_lt_int eqff_to_assert bool_cases_sqequal subtype_base_sq bool_wf bool_subtype_base assert-bnot iff_weakening_uiff assert_wf add-associates add-swap add-commutes zero-add add-subtract-cancel squash_wf istype-universe primrec0_lemma subtract_wf itermSubtract_wf int_term_value_subtract_lemma primrec-wf2
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :lambdaFormation_alt,  cut sqequalRule Error :functionIsType,  Error :universeIsType,  introduction extract_by_obid hypothesis sqequalHypSubstitution isectElimination thin productEquality applyEquality hypothesisEquality setElimination rename because_Cache Error :lambdaEquality_alt,  Error :inhabitedIsType,  Error :productIsType,  independent_isectElimination universeEquality dependent_functionElimination Error :dependent_set_memberEquality_alt,  addEquality natural_numberEquality unionElimination approximateComputation independent_functionElimination Error :dependent_pairFormation_alt,  int_eqEquality Error :isect_memberEquality_alt,  voidElimination independent_pairFormation productElimination imageElimination instantiate functionEquality equalityElimination equalityTransitivity equalitySymmetry Error :equalityIstype,  promote_hyp cumulativity hyp_replacement imageMemberEquality baseClosed applyLambdaEquality Error :setIsType

Latex:
\mforall{}A:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}.  ((\mforall{}s:StrictInc.  \00D9(\mexists{}n:\mBbbN{}.  A[s  n]))  {}\mRightarrow{}  \00D9(\mexists{}s:StrictInc.  \mforall{}n:\mBbbN{}.  A[s  n]))



Date html generated: 2019_06_20-PM-02_57_32
Last ObjectModification: 2019_02_06-PM-03_58_56

Theory : continuity


Home Index