Nuprl Lemma : last-full-partition
∀[I:Interval]. ∀[p:partition(I)]. (last(full-partition(I;p)) = right-endpoint(I) ∈ ℝ) supposing icompact(I)
Proof
Definitions occuring in Statement :
full-partition: full-partition(I;p),
partition: partition(I),
icompact: icompact(I),
right-endpoint: right-endpoint(I),
interval: Interval,
real: ℝ,
last: last(L),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
full-partition: full-partition(I;p),
squash: ↓T,
prop: ℙ,
partition: partition(I),
true: True,
subtype_rel: A ⊆r B,
guard: {T},
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
implies: P ⇒ Q,
icompact: icompact(I),
top: Top,
all: ∀x:A. B[x],
not: ¬A,
uiff: uiff(P;Q),
false: False
Lemmas referenced :
equal_wf,
squash_wf,
true_wf,
real_wf,
last_cons,
append_wf,
cons_wf,
right-endpoint_wf,
nil_wf,
left-endpoint_wf,
iff_weakening_equal,
partition_wf,
icompact_wf,
interval_wf,
null_append,
subtype_rel_list,
top_wf,
null_cons_lemma,
assert_of_ff,
assert_functionality_wrt_uiff,
band_wf,
null_wf3,
bfalse_wf,
band_ff_simp,
assert_wf,
not_wf,
last_append,
assert_elim,
btrue_neq_bfalse,
last_singleton
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
applyEquality,
thin,
lambdaEquality,
sqequalHypSubstitution,
imageElimination,
extract_by_obid,
isectElimination,
hypothesisEquality,
equalityTransitivity,
hypothesis,
equalitySymmetry,
universeEquality,
because_Cache,
setElimination,
rename,
independent_isectElimination,
natural_numberEquality,
sqequalRule,
imageMemberEquality,
baseClosed,
productElimination,
independent_functionElimination,
isect_memberEquality,
axiomEquality,
voidElimination,
voidEquality,
dependent_functionElimination,
addLevel,
impliesFunctionality,
lambdaFormation,
levelHypothesis
Latex:
\mforall{}[I:Interval]
\mforall{}[p:partition(I)]. (last(full-partition(I;p)) = right-endpoint(I)) supposing icompact(I)
Date html generated:
2017_10_03-AM-09_40_10
Last ObjectModification:
2017_07_28-AM-07_55_43
Theory : reals
Home
Index