Nuprl Lemma : member-rcc-min-max
∀[x,y,t:ℝ]. uiff(t ∈ [rmin(x;y), rmax(x;y)];(|t - x| ≤ |y - x|) ∧ (|t - y| ≤ |y - x|))
Proof
Definitions occuring in Statement :
rccint: [l, u],
i-member: r ∈ I,
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 :
all: ∀x:A. B[x],
member: t ∈ T
Latex:
\mforall{}[x,y,t:\mBbbR{}]. uiff(t \mmember{} [rmin(x;y), rmax(x;y)];(|t - x| \mleq{} |y - x|) \mwedge{} (|t - y| \mleq{} |y - x|))
Date html generated:
2020_05_20-AM-11_35_57
Last ObjectModification:
2019_12_20-PM-00_41_28
Theory : reals
Home
Index