Nuprl Lemma : i-finite-closed-is-rccint
∀[I:Interval]. I ~ [left-endpoint(I), right-endpoint(I)] supposing i-finite(I) ∧ i-closed(I)
Proof
Definitions occuring in Statement :
rccint: [l, u],
i-closed: i-closed(I),
right-endpoint: right-endpoint(I),
left-endpoint: left-endpoint(I),
i-finite: i-finite(I),
interval: Interval,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
and: P ∧ Q,
sqequal: s ~ t
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
and: P ∧ Q,
interval: Interval,
i-closed: i-closed(I),
isl: isl(x),
outl: outl(x),
bnot: ¬bb,
ifthenelse: if b then t else f fi ,
btrue: tt,
bor: p ∨bq,
bfalse: ff,
assert: ↑b,
i-finite: i-finite(I),
rccint: [l, u],
all: ∀x:A. B[x],
top: Top,
false: False,
prop: ℙ
Latex:
\mforall{}[I:Interval]. I \msim{} [left-endpoint(I), right-endpoint(I)] supposing i-finite(I) \mwedge{} i-closed(I)
Date html generated:
2020_05_20-AM-11_32_43
Last ObjectModification:
2019_12_06-PM-02_02_19
Theory : reals
Home
Index