Nuprl Lemma : iproper-subinterval
∀I,J:Interval. (I ⊆ J ⇒ iproper(I) ⇒ iproper(J))
Proof
Definitions occuring in Statement :
subinterval: I ⊆ J ,
iproper: iproper(I),
interval: Interval,
all: ∀x:A. B[x],
implies: P ⇒ Q
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
prop: ℙ,
icompact: icompact(I),
and: P ∧ Q,
iproper: iproper(I),
top: Top,
i-finite: i-finite(I),
rccint: [l, u],
isl: isl(x),
assert: ↑b,
ifthenelse: if b then t else f fi ,
btrue: tt,
cand: A c∧ B,
true: True,
subinterval: I ⊆ J ,
i-member: r ∈ I,
guard: {T},
rbetween: x≤y≤z,
i-nonvoid: i-nonvoid(I),
exists: ∃x:A. B[x],
iff: P ⇐⇒ Q
Latex:
\mforall{}I,J:Interval. (I \msubseteq{} J {}\mRightarrow{} iproper(I) {}\mRightarrow{} iproper(J))
Date html generated:
2020_05_20-AM-11_35_22
Last ObjectModification:
2019_12_06-AM-10_15_11
Theory : reals
Home
Index