Nuprl Lemma : implies-approx-compact
∀I:Interval. ∀n:ℕ+. ((∃r:ℝ. (r ∈ i-approx(I;n))) ⇒ icompact(i-approx(I;n)))
Proof
Definitions occuring in Statement :
icompact: icompact(I),
i-approx: i-approx(I;n),
i-member: r ∈ I,
interval: Interval,
real: ℝ,
nat_plus: ℕ+,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
exists: ∃x:A. B[x],
member: t ∈ T,
uall: ∀[x:A]. B[x],
prop: ℙ
Latex:
\mforall{}I:Interval. \mforall{}n:\mBbbN{}\msupplus{}. ((\mexists{}r:\mBbbR{}. (r \mmember{} i-approx(I;n))) {}\mRightarrow{} icompact(i-approx(I;n)))
Date html generated:
2020_05_20-AM-11_33_15
Last ObjectModification:
2019_12_13-AM-11_25_15
Theory : reals
Home
Index