### Nuprl Lemma : pseudo-bounded-not-unbounded

`∀[S:{S:Type| S ⊆r ℕ} ]. (pseudo-bounded(S) `` (¬(∀B:ℕ. ∃n:{B...}. (n ∈ S))))`

Proof

Definitions occuring in Statement :  pseudo-bounded: `pseudo-bounded(S)` int_upper: `{i...}` nat: `ℕ` subtype_rel: `A ⊆r B` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` not: `¬A` implies: `P `` Q` member: `t ∈ T` set: `{x:A| B[x]} ` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` sq_stable: `SqStable(P)` implies: `P `` Q` squash: `↓T` all: `∀x:A. B[x]` subtype_rel: `A ⊆r B` nat: `ℕ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` uimplies: `b supposing a` not: `¬A` false: `False` exists: `∃x:A. B[x]` int_upper: `{i...}` prop: `ℙ` pi1: `fst(t)` pseudo-bounded: `pseudo-bounded(S)` guard: `{T}` ge: `i ≥ j ` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` top: `Top` le: `A ≤ B` and: `P ∧ Q`
Lemmas referenced :  sq_stable__subtype_rel nat_wf set_subtype_base le_wf istype-int int_subtype_base equal-wf-base istype-universe int_upper_wf pseudo-bounded_wf subtype_rel_wf subtype_rel_self exists_wf nat_properties decidable__le full-omega-unsat intformnot_wf intformle_wf itermVar_wf int_formula_prop_not_lemma istype-void int_formula_prop_le_lemma int_term_value_var_lemma int_formula_prop_wf le_weakening2 decidable__lt subtype_rel_transitivity int_upper_properties intformand_wf intformless_wf int_formula_prop_and_lemma int_formula_prop_less_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin setElimination rename hypothesisEquality hypothesis independent_functionElimination sqequalRule imageMemberEquality baseClosed imageElimination Error :lambdaFormation_alt,  baseApply closedConclusion applyEquality intEquality Error :lambdaEquality_alt,  natural_numberEquality independent_isectElimination because_Cache equalityTransitivity equalitySymmetry Error :universeIsType,  promote_hyp productElimination Error :functionIsType,  Error :productIsType,  Error :equalityIsType4,  voidElimination Error :setIsType,  universeEquality Error :dependent_pairFormation_alt,  functionExtensionality Error :inhabitedIsType,  Error :equalityIsType1,  dependent_functionElimination Error :dependent_set_memberEquality_alt,  unionElimination approximateComputation int_eqEquality Error :isect_memberEquality_alt,  applyLambdaEquality independent_pairFormation

Latex:
\mforall{}[S:\{S:Type|  S  \msubseteq{}r  \mBbbN{}\}  ].  (pseudo-bounded(S)  {}\mRightarrow{}  (\mneg{}(\mforall{}B:\mBbbN{}.  \mexists{}n:\{B...\}.  (n  \mmember{}  S))))

Date html generated: 2019_06_20-PM-02_51_57
Last ObjectModification: 2018_10_05-PM-11_12_49

Theory : continuity

Home Index