Nuprl Lemma : mcompact-interval
∀a,b:ℝ. mcompact({x:ℝ| x ∈ [a, b]} ;rmetric()) supposing a ≤ b
Proof
Definitions occuring in Statement :
mcompact: mcompact(X;d)
,
rmetric: rmetric()
,
rccint: [l, u]
,
i-member: r ∈ I
,
rleq: x ≤ y
,
real: ℝ
,
uimplies: b supposing a
,
all: ∀x:A. B[x]
,
set: {x:A| B[x]}
Definitions unfolded in proof :
prop: ℙ
,
mcompact: mcompact(X;d)
,
and: P ∧ Q
,
le: A ≤ B
,
uall: ∀[x:A]. B[x]
,
rnonneg: rnonneg(x)
,
rleq: x ≤ y
,
member: t ∈ T
,
uimplies: b supposing a
,
all: ∀x:A. B[x]
Lemmas referenced :
real_wf,
rleq_wf,
real-interval-m-TB,
real-interval-complete,
le_witness_for_triv
Rules used in proof :
universeIsType,
dependent_set_memberEquality_alt,
independent_pairFormation,
rename,
inhabitedIsType,
functionIsTypeImplies,
independent_isectElimination,
equalitySymmetry,
hypothesis,
equalityTransitivity,
productElimination,
isectElimination,
extract_by_obid,
hypothesisEquality,
thin,
dependent_functionElimination,
lambdaEquality_alt,
sqequalHypSubstitution,
sqequalRule,
introduction,
cut,
isect_memberFormation_alt,
lambdaFormation_alt,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}a,b:\mBbbR{}. mcompact(\{x:\mBbbR{}| x \mmember{} [a, b]\} ;rmetric()) supposing a \mleq{} b
Date html generated:
2019_10_31-AM-06_00_21
Last ObjectModification:
2019_10_30-AM-11_26_03
Theory : reals
Home
Index