Nuprl Lemma : halfpi-half-pi
π/2 = π/2(slower)
Proof
Definitions occuring in Statement :
halfpi: π/2,
half-pi: π/2(slower),
req: x = y
Definitions unfolded in proof :
member: t ∈ T,
squash: ↓T,
uall: ∀[x:A]. B[x],
sq_stable: SqStable(P),
implies: P ⇒ Q
Lemmas referenced :
halfpi_wf1,
sq_stable__req,
half-pi_wf
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :applyLambdaEquality,
setElimination,
thin,
rename,
hypothesis,
sqequalRule,
imageMemberEquality,
hypothesisEquality,
baseClosed,
imageElimination,
isectElimination,
equalityTransitivity,
equalitySymmetry,
independent_functionElimination
Latex:
\mpi{}/2 = \mpi{}/2(slower)
Date html generated:
2016_10_26-PM-00_23_00
Last ObjectModification:
2016_09_12-PM-05_42_44
Theory : reals_2
Home
Index