Nuprl Lemma : arctangent_one_one
∀x,y:ℝ. x = y supposing arctangent(x) = arctangent(y)
Proof
Definitions occuring in Statement :
arctangent: arctangent(x),
req: x = y,
real: ℝ,
uimplies: b supposing a,
all: ∀x:A. B[x]
Definitions unfolded in proof :
all: ∀x:A. B[x],
uimplies: b supposing a,
member: t ∈ T,
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
prop: ℙ,
stable: Stable{P},
not: ¬A,
or: P ∨ Q,
false: False,
rneq: x ≠ y,
guard: {T}
Lemmas referenced :
req_witness,
req_wf,
arctangent_wf,
real_wf,
stable_req,
false_wf,
or_wf,
rneq_wf,
not_wf,
minimal-double-negation-hyp-elim,
minimal-not-not-excluded-middle,
arctangent_functionality_wrt_rless,
req_inversion,
rless_transitivity1,
rleq_weakening,
rless_irreflexivity,
not-rneq
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
isect_memberFormation,
introduction,
cut,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
independent_functionElimination,
hypothesis,
functionEquality,
because_Cache,
independent_isectElimination,
unionElimination,
voidElimination,
dependent_functionElimination
Latex:
\mforall{}x,y:\mBbbR{}. x = y supposing arctangent(x) = arctangent(y)
Date html generated:
2018_05_22-PM-03_02_14
Last ObjectModification:
2017_10_22-AM-00_26_03
Theory : reals_2
Home
Index