### Nuprl Lemma : bounded-decidable-nset-finite

`∀K:Type. ((K ⊆r ℕ) `` (∀l:ℕ. ((l ∈ K) ∨ (¬(l ∈ K)))) `` (∀B:ℕ. ((∀k:K. (k ≤ B)) `` finite(K))))`

Proof

Definitions occuring in Statement :  finite: `finite(T)` nat: `ℕ` subtype_rel: `A ⊆r B` le: `A ≤ B` all: `∀x:A. B[x]` not: `¬A` implies: `P `` Q` or: `P ∨ Q` member: `t ∈ T` universe: `Type`
Definitions unfolded in proof :  l_member: `(x ∈ l)` true: `True` cand: `A c∧ B` squash: `↓T` less_than: `a < b` bfalse: `ff` btrue: `tt` ifthenelse: `if b then t else f fi ` assert: `↑b` less_than': `less_than'(a;b)` isl: `isl(x)` prop: `ℙ` top: `Top` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` le: `A ≤ B` decidable: `Dec(P)` ge: `i ≥ j ` lelt: `i ≤ j < k` int_seg: `{i..j-}` false: `False` not: `¬A` so_apply: `x[s]` so_lambda: `λ2x.t[x]` or: `P ∨ Q` uimplies: `b supposing a` nat: `ℕ` guard: `{T}` subtype_rel: `A ⊆r B` rev_implies: `P `` Q` and: `P ∧ Q` iff: `P `⇐⇒` Q` member: `t ∈ T` uall: `∀[x:A]. B[x]` implies: `P `` Q` all: `∀x:A. B[x]`
Lemmas referenced :  select_wf length_wf change-equality-type subtype-base-respects-equality member_filter no_repeats-subtype no_repeats_upto int_seg_properties no_repeats_filter l_member_wf no_repeats_wf istype-assert istype-true assert_wf istype-false int_seg_subtype_nat int_seg_wf subtype_rel_list upto_wf bfalse_wf btrue_wf filter_type decidable__le member_upto istype-less_than int_formula_prop_wf int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_add_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma intformle_wf itermConstant_wf itermAdd_wf itermVar_wf intformless_wf intformnot_wf intformand_wf full-omega-unsat decidable__lt nat_properties zero-le-nat istype-universe subtype_rel_wf istype-void int_subtype_base istype-int le_wf set_subtype_base istype-nat nat_wf subtype_rel_transitivity istype-le finite-iff-listable
Rules used in proof :  promote_hyp imageElimination Error :setIsType,  setEquality equalityTransitivity functionExtensionality Error :productIsType,  voidElimination Error :isect_memberEquality_alt,  int_eqEquality Error :dependent_pairFormation_alt,  approximateComputation unionElimination addEquality dependent_functionElimination independent_pairFormation Error :dependent_set_memberEquality_alt,  universeEquality instantiate equalitySymmetry sqequalBase because_Cache natural_numberEquality Error :equalityIstype,  Error :unionIsType,  independent_isectElimination intEquality Error :inhabitedIsType,  rename setElimination Error :lambdaEquality_alt,  applyEquality Error :universeIsType,  Error :functionIsType,  sqequalRule independent_functionElimination productElimination hypothesis hypothesisEquality thin isectElimination sqequalHypSubstitution extract_by_obid introduction cut Error :lambdaFormation_alt,  sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}K:Type.  ((K  \msubseteq{}r  \mBbbN{})  {}\mRightarrow{}  (\mforall{}l:\mBbbN{}.  ((l  \mmember{}  K)  \mvee{}  (\mneg{}(l  \mmember{}  K))))  {}\mRightarrow{}  (\mforall{}B:\mBbbN{}.  ((\mforall{}k:K.  (k  \mleq{}  B))  {}\mRightarrow{}  finite(K))))

Date html generated: 2019_06_20-PM-03_02_18
Last ObjectModification: 2019_06_13-PM-03_57_08

Theory : continuity

Home Index