Nuprl Lemma : between-rmin-rmax
∀[x,y,t:ℝ]. uiff((rmin(x;y) ≤ t) ∧ (t ≤ rmax(x;y));(|t - x| ≤ |y - x|) ∧ (|t - y| ≤ |y - x|))
Proof
Definitions occuring in Statement :
rleq: x ≤ y,
rabs: |x|,
rmin: rmin(x;y),
rmax: rmax(x;y),
rsub: x - y,
real: ℝ,
uiff: uiff(P;Q),
uall: ∀[x:A]. B[x],
and: P ∧ Q
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
uiff: uiff(P;Q),
and: P ∧ Q,
uimplies: b supposing a,
member: t ∈ T,
prop: ℙ,
implies: P ⇒ Q,
sq_stable: SqStable(P),
rleq: x ≤ y,
rnonneg: rnonneg(x),
all: ∀x:A. B[x],
le: A ≤ B,
squash: ↓T,
or: P ∨ Q,
guard: {T},
rev_uimplies: rev_uimplies(P;Q),
rge: x ≥ y,
cand: A c∧ B,
rev_implies: P ⇐ Q,
iff: P ⇐⇒ Q,
not: ¬A,
false: False,
stable: Stable{P},
req_int_terms: t1 ≡ t2
Latex:
\mforall{}[x,y,t:\mBbbR{}]. uiff((rmin(x;y) \mleq{} t) \mwedge{} (t \mleq{} rmax(x;y));(|t - x| \mleq{} |y - x|) \mwedge{} (|t - y| \mleq{} |y - x|))
Date html generated:
2020_05_20-AM-11_35_41
Last ObjectModification:
2019_12_20-PM-00_38_35
Theory : reals
Home
Index