Nuprl Lemma : totally-bounded-bounded-above

[A:Set(ℝ)]. (totally-bounded(A)  bounded-above(A))

Proof

Definitions occuring in Statement :  totally-bounded: totally-bounded(A) bounded-above: bounded-above(A) rset: Set(ℝ) uall: [x:A]. B[x] implies:  Q
Definitions unfolded in proof :  bounded-above: bounded-above(A) totally-bounded: totally-bounded(A) uall: [x:A]. B[x] implies:  Q all: x:A. B[x] member: t ∈ T iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q less_than: a < b squash: T less_than': less_than'(a;b) true: True exists: x:A. B[x] prop: nat_plus: + uimplies: supposing a decidable: Dec(P) or: P ∨ Q not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) false: False top: Top so_lambda: λ2x.t[x] int_seg: {i..j-} lelt: i ≤ j < k so_apply: x[s] upper-bound: A ≤ b cand: c∧ B guard: {T} le: A ≤ B subtype_rel: A ⊆B uiff: uiff(P;Q) req_int_terms: t1 ≡ t2 rev_uimplies: rev_uimplies(P;Q) rless: x < y sq_exists: x:A [B[x]] real: sq_stable: SqStable(P) subtract: m sq_type: SQType(T)
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation_alt lambdaFormation_alt cut hypothesis sqequalHypSubstitution dependent_functionElimination thin introduction extract_by_obid isectElimination natural_numberEquality independent_functionElimination productElimination independent_pairFormation imageMemberEquality hypothesisEquality baseClosed functionIsType universeIsType productIsType setElimination rename because_Cache applyEquality dependent_pairFormation_alt closedConclusion independent_isectElimination unionElimination approximateComputation lambdaEquality_alt int_eqEquality isect_memberEquality_alt voidElimination dependent_set_memberEquality_alt addEquality imageElimination equalityTransitivity equalitySymmetry inhabitedIsType instantiate universeEquality cumulativity intEquality

Latex:
\mforall{}[A:Set(\mBbbR{})].  (totally-bounded(A)  {}\mRightarrow{}  bounded-above(A))

Date html generated: 2019_10_29-AM-10_43_50
Last ObjectModification: 2019_04_19-PM-06_12_46

Theory : reals

Home Index