Nuprl Lemma : rless*_functionality_wrt_implies
∀a,b,c,d:ℝ*. (b ≥ a ⇒ c ≤ d ⇒ {b < c ⇒ a < d})
Proof
Definitions occuring in Statement :
rge*: x ≥ y,
rleq*: x ≤ y,
rless*: x < y,
real*: ℝ*,
guard: {T},
all: ∀x:A. B[x],
implies: P ⇒ Q
Definitions unfolded in proof :
rge*: x ≥ y,
all: ∀x:A. B[x],
implies: P ⇒ Q,
guard: {T},
member: t ∈ T,
prop: ℙ,
uall: ∀[x:A]. B[x]
Lemmas referenced :
rless*_wf,
rleq*_wf,
real*_wf,
rless*_transitivity1,
rless*_transitivity2
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
lambdaFormation,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
dependent_functionElimination,
independent_functionElimination
Latex:
\mforall{}a,b,c,d:\mBbbR{}*. (b \mgeq{} a {}\mRightarrow{} c \mleq{} d {}\mRightarrow{} \{b < c {}\mRightarrow{} a < d\})
Date html generated:
2018_05_22-PM-09_28_17
Last ObjectModification:
2017_10_10-PM-01_42_35
Theory : reals_2
Home
Index