Nuprl Lemma : req_witness
∀[x,y:ℝ]. ((x = y) ⇒ (λn.<λ_.Ax, Ax, Ax> ∈ x = y))
Proof
Definitions occuring in Statement :
req: x = y,
real: ℝ,
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
member: t ∈ T,
lambda: λx.A[x],
pair: <a, b>,
axiom: Ax
Definitions unfolded in proof :
req: x = y,
uall: ∀[x:A]. B[x],
member: t ∈ T,
implies: P ⇒ Q,
all: ∀x:A. B[x],
le: A ≤ B,
and: P ∧ Q,
real: ℝ,
subtype_rel: A ⊆r B,
top: Top,
uimplies: b supposing a,
not: ¬A,
prop: ℙ,
guard: {T}
Lemmas referenced :
member-not,
less_than'_wf,
absval_wf,
subtract_wf,
istype-void,
nat_plus_wf,
istype-le,
real_wf
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
isect_memberFormation_alt,
introduction,
cut,
lambdaFormation_alt,
lambdaEquality_alt,
independent_pairEquality,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
closedConclusion,
natural_numberEquality,
applyEquality,
setElimination,
rename,
because_Cache,
hypothesis,
hypothesisEquality,
isect_memberEquality_alt,
voidElimination,
independent_isectElimination,
universeIsType,
axiomEquality,
functionIsType,
dependent_functionElimination,
equalityTransitivity,
equalitySymmetry,
functionIsTypeImplies,
inhabitedIsType,
isectIsTypeImplies,
productElimination,
independent_functionElimination
Latex:
\mforall{}[x,y:\mBbbR{}]. ((x = y) {}\mRightarrow{} (\mlambda{}n.<\mlambda{}$_{}$.Ax, Ax, Ax> \mmember{} x = y))
Date html generated:
2019_10_16-PM-03_07_06
Last ObjectModification:
2018_11_08-PM-05_56_58
Theory : reals
Home
Index