Nuprl Lemma : trivial-subinterval
∀I:Interval. [left-endpoint(I), right-endpoint(I)] ⊆ I supposing icompact(I)
Proof
Definitions occuring in Statement :
subinterval: I ⊆ J ,
icompact: icompact(I),
rccint: [l, u],
right-endpoint: right-endpoint(I),
left-endpoint: left-endpoint(I),
interval: Interval,
uimplies: b supposing a,
all: ∀x:A. B[x]
Definitions unfolded in proof :
icompact: icompact(I),
cand: A c∧ B,
rev_implies: P ⇐ Q,
and: P ∧ Q,
iff: P ⇐⇒ Q,
uall: ∀[x:A]. B[x],
prop: ℙ,
squash: ↓T,
implies: P ⇒ Q,
sq_stable: SqStable(P),
member: t ∈ T,
uimplies: b supposing a,
all: ∀x:A. B[x]
Lemmas referenced :
rleq_wf,
icompact-endpoints,
right-endpoint_wf,
left-endpoint_wf,
rcc-subinterval,
interval_wf,
icompact_wf,
sq_stable__icompact
Rules used in proof :
independent_pairFormation,
productElimination,
because_Cache,
independent_isectElimination,
isectElimination,
imageElimination,
baseClosed,
imageMemberEquality,
sqequalRule,
independent_functionElimination,
hypothesis,
hypothesisEquality,
thin,
dependent_functionElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
cut,
isect_memberFormation,
lambdaFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}I:Interval. [left-endpoint(I), right-endpoint(I)] \msubseteq{} I supposing icompact(I)
Date html generated:
2018_07_29-AM-09_40_05
Last ObjectModification:
2018_07_02-PM-00_27_01
Theory : reals
Home
Index