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