Nuprl Lemma : not-qle
∀[q,r:ℚ]. ((¬(q ≤ r)) ⇒ r < q)
Proof
Definitions occuring in Statement :
qle: r ≤ s,
qless: r < s,
rationals: ℚ,
uall: ∀[x:A]. B[x],
not: ¬A,
implies: P ⇒ Q
Definitions unfolded in proof :
false: False,
prop: ℙ,
not: ¬A,
uimplies: b supposing a,
and: P ∧ Q,
uiff: uiff(P;Q),
implies: P ⇒ Q,
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
rationals_wf,
qless_witness,
istype-void,
qle_wf,
qle_complement_qorder
Rules used in proof :
isectIsTypeImplies,
because_Cache,
isect_memberEquality_alt,
inhabitedIsType,
functionIsTypeImplies,
independent_functionElimination,
dependent_functionElimination,
lambdaEquality_alt,
universeIsType,
functionIsType,
sqequalRule,
hypothesis,
independent_isectElimination,
productElimination,
hypothesisEquality,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
lambdaFormation_alt,
cut,
introduction,
isect_memberFormation_alt,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[q,r:\mBbbQ{}]. ((\mneg{}(q \mleq{} r)) {}\mRightarrow{} r < q)
Date html generated:
2019_10_29-AM-07_43_47
Last ObjectModification:
2019_10_21-PM-06_22_25
Theory : rationals
Home
Index