### Nuprl Lemma : ccc-nset-iff-finite

`∀K:Type. ((K ⊆r ℕ) `` K `` (CCC(K) `⇐⇒` finite(K)))`

Proof

Definitions occuring in Statement :  contra-cc: `CCC(T)` finite: `finite(T)` nat: `ℕ` subtype_rel: `A ⊆r B` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` implies: `P `` Q` universe: `Type`
Definitions unfolded in proof :  so_apply: `x[s1;s2]` so_lambda: `λ2x y.t[x; y]` squash: `↓T` less_than: `a < b` lelt: `i ≤ j < k` int_seg: `{i..j-}` l_exists: `(∃x∈L. P[x])` satisfiable_int_formula: `satisfiable_int_formula(fmla)` ge: `i ≥ j ` sq_type: `SQType(T)` l_member: `(x ∈ l)` true: `True` less_than': `less_than'(a;b)` subtract: `n - m` uiff: `uiff(P;Q)` decidable: `Dec(P)` le: `A ≤ B` top: `Top` cons: `[a / b]` or: `P ∨ Q` rev_implies: `P `` Q` uimplies: `b supposing a` nat: `ℕ` guard: `{T}` subtype_rel: `A ⊆r B` exists: `∃x:A. B[x]` prop: `ℙ` uall: `∀[x:A]. B[x]` false: `False` not: `¬A` member: `t ∈ T` cand: `A c∧ B` ccc-nset: `CCCNSet(K)` and: `P ∧ Q` iff: `P `⇐⇒` Q` implies: `P `` Q` all: `∀x:A. B[x]`
Lemmas referenced :  CCC-Sigma02-dns int_formula_prop_less_lemma intformless_wf int_seg_properties le_wf length_wf istype-less_than int_formula_prop_wf int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma istype-int itermVar_wf itermConstant_wf intformle_wf intformnot_wf intformand_wf full-omega-unsat decidable__le nat_properties select_wf int_subtype_base subtype_base_sq imax-list-ub subtype_rel_list imax-list-member le-add-cancel add-zero add-associates add_functionality_wrt_le add-commutes minus-one-mul-top zero-add minus-one-mul minus-add condition-implies-le not-lt-2 istype-false decidable__lt length_wf_nat length_of_cons_lemma product_subtype_list nil_member length_of_nil_lemma list-cases finite-iff-listable istype-universe subtype_rel_wf CCC-finite contra-cc_wf bounded-ccc-nset-finite istype-void nat_wf subtype_rel_transitivity istype-nat istype-le finite_wf ccc-nset-not-not-finite
Rules used in proof :  imageElimination applyLambdaEquality hyp_replacement Error :dependent_set_memberEquality_alt,  int_eqEquality approximateComputation cumulativity Error :dependent_pairFormation_alt,  equalitySymmetry equalityTransitivity Error :equalityIstype,  minusEquality addEquality natural_numberEquality Error :isect_memberEquality_alt,  hypothesis_subsumption promote_hyp unionElimination universeEquality instantiate productElimination independent_isectElimination intEquality rename setElimination Error :lambdaEquality_alt,  applyEquality because_Cache Error :inhabitedIsType,  Error :productIsType,  Error :functionIsType,  sqequalRule isectElimination Error :universeIsType,  voidElimination independent_functionElimination hypothesisEquality thin dependent_functionElimination sqequalHypSubstitution extract_by_obid introduction hypothesis cut independent_pairFormation Error :lambdaFormation_alt,  sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}K:Type.  ((K  \msubseteq{}r  \mBbbN{})  {}\mRightarrow{}  K  {}\mRightarrow{}  (CCC(K)  \mLeftarrow{}{}\mRightarrow{}  finite(K)))

Date html generated: 2019_06_20-PM-03_03_04
Last ObjectModification: 2019_06_14-AM-10_08_41

Theory : continuity

Home Index