### Nuprl Lemma : pseudo-bounded-is-bounded

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

Proof

Definitions occuring in Statement :  pseudo-bounded: `pseudo-bounded(S)` quotient: `x,y:A//B[x; y]` nat: `ℕ` subtype_rel: `A ⊆r B` uall: `∀[x:A]. B[x]` le: `A ≤ B` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` true: `True` set: `{x:A| B[x]} ` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` sq_stable: `SqStable(P)` squash: `↓T` pseudo-bounded: `pseudo-bounded(S)` exists: `∃x:A. B[x]` and: `P ∧ Q` prop: `ℙ` uimplies: `b supposing a` so_lambda: `λ2x.t[x]` nat: `ℕ` subtype_rel: `A ⊆r B` int_upper: `{i...}` so_apply: `x[s]` guard: `{T}` le: `A ≤ B` less_than': `less_than'(a;b)` false: `False` not: `¬A` pi1: `fst(t)` ge: `i ≥ j ` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` top: `Top` int_seg: `{i..j-}` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` ifthenelse: `if b then t else f fi ` bfalse: `ff` sq_type: `SQType(T)` bnot: `¬bb` assert: `↑b` lelt: `i ≤ j < k` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` less_than: `a < b`
Lemmas referenced :  sq_stable__subtype_rel nat_wf weak-continuity-truncated subtype_rel_wf squash_wf pseudo-bounded_wf exists_wf all_wf int_upper_wf less_than_wf int_upper_subtype_nat subtype_rel_transitivity equal_wf int_seg_wf subtype_rel_dep_function int_seg_subtype_nat false_wf subtype_rel_self le_wf implies-quotient-true imax_wf imax_nat nat_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf intformeq_wf 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_eq_lemma int_formula_prop_wf less_than'_wf ifthenelse_wf lt_int_wf bool_wf eqtt_to_assert assert_of_lt_int eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot int_seg_properties intformless_wf int_formula_prop_less_lemma set_subtype_base int_subtype_base assert_wf bnot_wf not_wf imax_ub bool_cases iff_transitivity iff_weakening_uiff assert_of_bnot
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin because_Cache hypothesis independent_functionElimination sqequalRule imageMemberEquality hypothesisEquality baseClosed imageElimination promote_hyp productElimination setElimination rename dependent_set_memberEquality independent_pairFormation productEquality cumulativity dependent_functionElimination independent_isectElimination setEquality universeEquality functionEquality applyEquality functionExtensionality lambdaEquality intEquality natural_numberEquality dependent_pairFormation equalityTransitivity equalitySymmetry applyLambdaEquality unionElimination int_eqEquality isect_memberEquality voidElimination voidEquality computeAll independent_pairEquality axiomEquality equalityElimination instantiate inlFormation impliesFunctionality inrFormation

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

Date html generated: 2017_04_17-AM-09_54_48
Last ObjectModification: 2017_02_27-PM-05_49_24

Theory : continuity

Home Index