Nuprl Lemma : reals-connected-ext
Connected(ℝ)
Proof
Definitions occuring in Statement :
connected: Connected(X),
real: ℝ
Definitions unfolded in proof :
member: t ∈ T,
ifthenelse: if b then t else f fi ,
subtract: n - m,
spreadn: spread3,
isl: isl(x),
btrue: tt,
it: ⋅,
bfalse: ff,
let: let,
isr: isr(x),
decdr-to-bool: bool(d),
pi1: fst(t),
pi2: snd(t),
cover-real: cover-real(d; a; b; cb),
accelerate: accelerate(k;f),
altered-seq1: altered-seq1(d; a; b; x; n),
blended-real: blended-real(k;x;y),
outl: outl(x),
altered-seq2: altered-seq2(d; a; b; x; n),
outr: outr(x),
cover-search-left: cover-search-left(d;a;b;x),
WCPR: WCPR(F;x;G),
WCP: WCP(F;f;G),
mu: mu(f),
mu-ge: mu-ge(f;n),
eq_bool: p =b q,
bor: p ∨bq,
band: p ∧b q,
cover-search-right: cover-search-right(d;a;b;x),
reals-connected,
inhabited-covers-real-implies-ext,
assert_functionality_wrt_uiff,
connectedness-main-lemma-ext,
uall: ∀[x:A]. B[x],
so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]),
so_apply: x[s1;s2;s3;s4],
so_lambda: λ2x y.t[x; y],
top: Top,
so_apply: x[s1;s2],
uimplies: b supposing a,
so_lambda: λ2x.t[x],
so_apply: x[s]
Lemmas referenced :
reals-connected,
lifting-strict-callbyvalue,
istype-void,
strict4-spread,
lifting-strict-decide,
strict4-decide,
inhabited-covers-real-implies-ext,
assert_functionality_wrt_uiff,
connectedness-main-lemma-ext
Rules used in proof :
introduction,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
instantiate,
extract_by_obid,
hypothesis,
sqequalRule,
thin,
sqequalHypSubstitution,
equalityTransitivity,
equalitySymmetry,
isectElimination,
baseClosed,
isect_memberEquality_alt,
voidElimination,
independent_isectElimination
Latex:
Connected(\mBbbR{})
Date html generated:
2019_10_30-AM-07_37_15
Last ObjectModification:
2019_10_10-AM-11_48_44
Theory : reals
Home
Index