Nuprl Lemma : rmin3-rmax3-subinterval
∀I:Interval. ∀a,b,c:ℝ. ((a ∈ I) ⇒ (b ∈ I) ⇒ (c ∈ I) ⇒ [rmin(a;rmin(b;c)), rmax(a;rmax(b;c))] ⊆ I )
Proof
Definitions occuring in Statement :
subinterval: I ⊆ J ,
rccint: [l, u],
i-member: r ∈ I,
interval: Interval,
rmin: rmin(x;y),
rmax: rmax(x;y),
real: ℝ,
all: ∀x:A. B[x],
implies: P ⇒ Q
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
member: t ∈ T,
uall: ∀[x:A]. B[x],
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
cand: A c∧ B,
prop: ℙ
Lemmas referenced :
rcc-subinterval,
rmin_wf,
rmax_wf,
rmin-i-member,
rmax-i-member,
rleq_wf,
i-member_wf,
real_wf,
interval_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
isectElimination,
hypothesis,
productElimination,
independent_functionElimination,
because_Cache,
independent_pairFormation
Latex:
\mforall{}I:Interval. \mforall{}a,b,c:\mBbbR{}.
((a \mmember{} I) {}\mRightarrow{} (b \mmember{} I) {}\mRightarrow{} (c \mmember{} I) {}\mRightarrow{} [rmin(a;rmin(b;c)), rmax(a;rmax(b;c))] \msubseteq{} I )
Date html generated:
2016_10_26-AM-09_31_28
Last ObjectModification:
2016_08_23-PM-01_15_19
Theory : reals
Home
Index