Nuprl Lemma : icompact-is-rccint
∀[I:Interval]. I ~ [left-endpoint(I), right-endpoint(I)] supposing icompact(I)
Proof
Definitions occuring in Statement :
icompact: icompact(I),
rccint: [l, u],
right-endpoint: right-endpoint(I),
left-endpoint: left-endpoint(I),
interval: Interval,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
sqequal: s ~ t
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
and: P ∧ Q,
cand: A c∧ B,
prop: ℙ,
icompact: icompact(I)
Latex:
\mforall{}[I:Interval]. I \msim{} [left-endpoint(I), right-endpoint(I)] supposing icompact(I)
Date html generated:
2020_05_20-AM-11_32_59
Last ObjectModification:
2019_12_06-PM-02_03_41
Theory : reals
Home
Index