Nuprl Lemma : inf_functionality
∀[A,A':Set(ℝ)]. ∀b,b':ℝ. ((b = b') ⇒ rseteq(A;A') ⇒ (inf(A) = b ⇐⇒ inf(A') = b'))
Proof
Definitions occuring in Statement :
inf: inf(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,
inf: inf(A) = b,
and: P ∧ Q,
lower-bound: lower-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{} (inf(A) = b \mLeftarrow{}{}\mRightarrow{} inf(A') = b'))
Date html generated:
2020_05_20-AM-11_27_57
Last ObjectModification:
2020_01_06-PM-00_19_00
Theory : reals
Home
Index