Nuprl Lemma : sup_functionality
∀[A,A':Set(ℝ)]. ∀b,b':ℝ. ((b = b') ⇒ rseteq(A;A') ⇒ (sup(A) = b ⇐⇒ sup(A') = b'))
Proof
Definitions occuring in Statement :
sup: sup(A) = b,
rseteq: rseteq(A;B),
rset: Set(ℝ),
req: x = y,
real: ℝ,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
implies: P ⇒ Q
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
sup: sup(A) = b,
and: P ∧ Q,
upper-bound: A ≤ b,
member: t ∈ T,
guard: {T},
uimplies: b supposing a,
prop: ℙ,
exists: ∃x:A. B[x],
cand: A c∧ B,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
rseteq: rseteq(A;B)
Latex:
\mforall{}[A,A':Set(\mBbbR{})]. \mforall{}b,b':\mBbbR{}. ((b = b') {}\mRightarrow{} rseteq(A;A') {}\mRightarrow{} (sup(A) = b \mLeftarrow{}{}\mRightarrow{} sup(A') = b'))
Date html generated:
2020_05_20-AM-11_28_15
Last ObjectModification:
2020_01_06-PM-00_19_15
Theory : reals
Home
Index