Logiweb codex of sup in pyk

Up Help

ref-3-id-28	Nat( {MissingArg} )
ref-3-id-63	meta-sub {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-3-id-64	meta-sub1 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-3-id-65	meta-sub* {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-3-id-350	lemma eqLeq(R)
ref-3-id-420	{MissingArg} ^ {MissingArg}
ref-0-id-0	sup
ref-0-id-1	prop lemma to negated and(1)
ref-0-id-2	lemma uniqueNegative
ref-0-id-3	lemma doubleMinus
ref-0-id-4	lemma minusNegated
ref-0-id-5	lemma eqReflexivity
ref-0-id-6	lemma eqSymmetry
ref-0-id-7	lemma eqTransitivity
ref-0-id-8	lemma eqTransitivity4
ref-0-id-9	lemma eqTransitivity5
ref-0-id-10	lemma eqTransitivity6
ref-0-id-11	lemma addEquations
ref-0-id-12	lemma subtractEquations
ref-0-id-13	lemma subtractEquationsLeft
ref-0-id-14	lemma multiplyEquations
ref-0-id-15	lemma eqNegated
ref-0-id-16	lemma positiveToRight(Eq)
ref-0-id-17	lemma positiveToLeft(Eq)(1 term)
ref-0-id-18	lemma negativeToLeft(Eq)
ref-0-id-19	lemma nonreciprocalToRight(Eq)(1 term)
ref-0-id-20	lemma plusAssociativity(4 terms)
ref-0-id-21	lemma lessNeq
ref-0-id-22	lemma neqSymmetry
ref-0-id-23	lemma neqNegated
ref-0-id-24	lemma subNeqRight
ref-0-id-25	lemma subNeqLeft
ref-0-id-26	lemma negativeToRight(Neq)(1 term)
ref-0-id-27	lemma neqAddition
ref-0-id-28	lemma neqMultiplication
ref-0-id-29	lemma nonzeroProduct(2)
ref-0-id-30	lemma UStelescope(+1)
ref-0-id-31	lemma telescopeBound base
ref-0-id-32	lemma telescopeBound indu
ref-0-id-33	lemma telescopeBound
ref-0-id-34	lemma intervalSize base
ref-0-id-35	lemma intervalSize indu
ref-0-id-36	lemma intervalSize
ref-0-id-37	lemma XSlessUS
ref-0-id-38	lemma USdecreasing(+1)
ref-0-id-39	lemma closeUS
ref-0-id-40	lemma closeUS(n+1)
ref-0-id-41	pred lemma allNegated(Imply)
ref-0-id-42	pred lemma existNegated(Imply)
ref-0-id-43	pred lemma intro exist helper
ref-0-id-44	pred lemma intro exist
ref-0-id-45	pred lemma exist mp
ref-0-id-46	pred lemma exist mp2
ref-0-id-47	pred lemma 2exist mp
ref-0-id-48	pred lemma 2exist mp2
ref-0-id-49	pred lemma EAE mp
ref-0-id-50	pred lemma addAll
ref-0-id-51	pred lemma addExist helper1
ref-0-id-52	pred lemma addExist helper2
ref-0-id-53	pred lemma addExist
ref-0-id-54	pred lemma addExist(SimpleAnt)
ref-0-id-55	pred lemma addExist(Simple)
ref-0-id-56	pred lemma addEAE
ref-0-id-57	pred lemma AEAnegated
ref-0-id-58	pred lemma EEAnegated
ref-0-id-59	lemma induction
ref-0-id-60	lemma leqAntisymmetry
ref-0-id-61	lemma leqTransitivity
ref-0-id-62	lemma leqAddition
ref-0-id-63	lemma leqMultiplication
ref-0-id-64	lemma reciprocal
ref-0-id-65	lemma equality
ref-0-id-66	lemma eqLeq
ref-0-id-67	lemma eqAddition
ref-0-id-68	lemma eqMultiplication
ref-0-id-69	lemma leqMultiplicationLeft
ref-0-id-70	lemma leqLessEq
ref-0-id-71	lemma lessLeq
ref-0-id-72	lemma from leqGeq
ref-0-id-73	lemma subLeqRight
ref-0-id-74	lemma subLeqLeft
ref-0-id-75	lemma leqPlus1
ref-0-id-76	lemma positiveToRight(Leq)
ref-0-id-77	lemma positiveToRight(Leq)(1 term)
ref-0-id-78	lemma negativeToRight(Leq)
ref-0-id-79	lemma positiveToLeft(Leq)
ref-0-id-80	lemma negativeToLeft(Leq)
ref-0-id-81	lemma negativeToLeft(Leq)(1 term)
ref-0-id-82	lemma leqAdditionLeft
ref-0-id-83	lemma leqSubtraction
ref-0-id-84	lemma leqSubtractionLeft
ref-0-id-85	lemma thirdGeq
ref-0-id-86	lemma leqNegated
ref-0-id-87	lemma addEquations(Leq)
ref-0-id-88	lemma multiplyEquations(Leq)
ref-0-id-89	lemma thirdGeqSeries
ref-0-id-90	lemma leqNeqLess
ref-0-id-91	lemma fromLess
ref-0-id-92	lemma toLess
ref-0-id-93	lemma fromNotLess
ref-0-id-94	lemma toNotLess
ref-0-id-95	lemma negativeLessPositive
ref-0-id-96	lemma leqLessTransitivity
ref-0-id-97	lemma lessLeqTransitivity
ref-0-id-98	lemma lessTransitivity
ref-0-id-99	lemma lessTotality
ref-0-id-100	lemma subLessRight
ref-0-id-101	lemma subLessLeft
ref-0-id-102	lemma switchTerms(x
ref-0-id-103	lemma switchTerms(x-y
ref-0-id-104	lemma lessAddition
ref-0-id-105	lemma lessAdditionLeft
ref-0-id-106	lemma lessMultiplication
ref-0-id-107	lemma lessMultiplicationLeft
ref-0-id-108	lemma lessDivision
ref-0-id-109	lemma positiveToRight(Less)
ref-0-id-110	lemma positiveToLeft(Less)
ref-0-id-111	lemma negativeToLeft(Less)
ref-0-id-112	lemma negativeToRight(Less)
ref-0-id-113	lemma addEquations(Less)
ref-0-id-114	lemma addEquations(LeqLess)
ref-0-id-115	lemma reciprocalToLeft(Less)
ref-0-id-116	lemma lessNegated
ref-0-id-117	lemma positiveNonzero
ref-0-id-118	lemma positiveNegated
ref-0-id-119	lemma nonpositiveNegated
ref-0-id-120	lemma negativeNegated
ref-0-id-121	lemma nonnegativeNegated
ref-0-id-122	lemma positiveHalved
ref-0-id-123	lemma positiveInverted
ref-0-id-124	lemma nonnegativeNumerical
ref-0-id-125	lemma negativeNumerical
ref-0-id-126	lemma positiveNumerical
ref-0-id-127	lemma nonpositiveNumerical
ref-0-id-128	lemma |0|=0
ref-0-id-129	lemma 0<=|x|
ref-0-id-130	lemma x<=|x|
ref-0-id-131	lemma fromPositiveNumerical
ref-0-id-132	lemma sameNumerical
ref-0-id-133	lemma signNumerical(+)
ref-0-id-134	lemma signNumerical
ref-0-id-135	lemma toNumericalLess
ref-0-id-136	lemma fromNumericalGreater
ref-0-id-137	lemma numericalDifference
ref-0-id-138	lemma numericalDifferenceLess helper
ref-0-id-139	lemma numericalDifferenceLess
ref-0-id-140	lemma splitNumericalSumHelper
ref-0-id-141	lemma splitNumericalSum(++)
ref-0-id-142	lemma splitNumericalSum(--)
ref-0-id-143	lemma splitNumericalSum(+-, smallNegative)
ref-0-id-144	lemma splitNumericalSum(+-, bigNegative)
ref-0-id-145	lemma splitNumericalSum(+-)
ref-0-id-146	lemma splitNumericalSum(-+)
ref-0-id-147	lemma splitNumericalSum
ref-0-id-148	lemma splitNumericalProduct(++)
ref-0-id-149	lemma splitNumericalProduct(+-)
ref-0-id-150	lemma splitNumericalProduct
ref-0-id-151	lemma insertMiddleTerm(Numerical)
ref-0-id-152	lemma insertTwoMiddleTerms(Numerical)
ref-0-id-153	lemma three2twoTerms
ref-0-id-154	lemma three2threeTerms
ref-0-id-155	lemma three2twoFactors
ref-0-id-156	lemma three2threeFactors
ref-0-id-157	lemma times(-1)
ref-0-id-158	lemma times(-1)Left
ref-0-id-159	lemma leqMax1
ref-0-id-160	lemma leqMax2
ref-0-id-161	lemma lessThanMax
ref-0-id-162	lemma x+y=zBackwards
ref-0-id-163	lemma x*y=zBackwards
ref-0-id-164	lemma x=x+(y-y)
ref-0-id-165	lemma x=x+y-y
ref-0-id-166	lemma x=x*y*(1/y)
ref-0-id-167	lemma insertMiddleTerm(Sum)
ref-0-id-168	lemma insertTwoMiddleTerms(Sum)
ref-0-id-169	lemma insertMiddleTerm(Difference)
ref-0-id-170	lemma x*0+x=x
ref-0-id-171	lemma x*0=0
ref-0-id-172	lemma nonnegativeFactors
ref-0-id-173	lemma nonzeroFactors
ref-0-id-174	lemma positiveFactors
ref-0-id-175	lemma plusTimesMinus
ref-0-id-176	lemma minusTimesMinus
ref-0-id-177	lemma (-1)*(-1)+(-1)*1=0
ref-0-id-178	lemma (-1)*(-1)=1
ref-0-id-179	lemma 0<1Helper
ref-0-id-180	lemma 0<1
ref-0-id-181	lemma 0<2
ref-0-id-182	lemma 0<3
ref-0-id-183	lemma 0<1/2
ref-0-id-184	lemma 0<1/3
ref-0-id-185	lemma x+x=2*x
ref-0-id-186	lemma x+x+x=3*x
ref-0-id-187	lemma (1/2)x+(1/2)x=x
ref-0-id-188	lemma (1/3)x+(1/3)x+(1/3)x=x
ref-0-id-189	lemma -x-y=-(x+y)
ref-0-id-190	lemma -x*y=-(x*y)
ref-0-id-191	lemma -0=0
ref-0-id-192	lemma sameFsymmetry
ref-0-id-193	lemma sameFtransitivity
ref-0-id-194	lemma f2R(Plus)
ref-0-id-195	lemma f2R(Times)
ref-0-id-196	lemma <
ref-0-id-197	lemma <
ref-0-id-198	lemma <<==Reflexivity
ref-0-id-199	lemma <<==AntisymmetryHelper(Q)
ref-0-id-200	lemma fromNot
ref-0-id-201	lemma fromNot
ref-0-id-202	lemma fromNot
ref-0-id-203	lemma fromNot
ref-0-id-204	lemma fromNot
ref-0-id-205	lemma fromNotSameF(Strongest) helper2
ref-0-id-206	lemma fromNotSameF(Strongest) helper
ref-0-id-207	lemma fromNotSameF(Strongest)
ref-0-id-208	lemma toLess(F) helper
ref-0-id-209	lemma toLess(F)
ref-0-id-210	lemma fromNot<<
ref-0-id-211	lemma toLess(R)
ref-0-id-212	lemma fromNotSameF(Weak)(Helper)
ref-0-id-213	lemma fromNotSameF(Weak)
ref-0-id-214	lemma fromNotLess(F)
ref-0-id-215	lemma ==Addition
ref-0-id-216	lemma ==AdditionLeft
ref-0-id-217	lemma fpart-Bounded base
ref-0-id-218	lemma fpart-Bounded indu helper
ref-0-id-219	lemma fpart-Bounded indu
ref-0-id-220	lemma fpart-Bounded
ref-0-id-221	lemma f-Bounded helper
ref-0-id-222	lemma f-Bounded
ref-0-id-223	lemma sameFmultiplication helper
ref-0-id-224	lemma sameFmultiplication
ref-0-id-225	lemma eqMultiplication(R)
ref-0-id-226	lemma eqMultiplicationLeft(R)
ref-0-id-227	lemma x*0=0(F)
ref-0-id-228	lemma x*0=0(R)
ref-0-id-229	lemma lessMultiplication(F) helper2
ref-0-id-230	lemma lessMultiplication(F) helper
ref-0-id-231	lemma lessMultiplication(F)
ref-0-id-232	lemma lessMultiplication(R)
ref-0-id-233	lemma leqMultiplication(R)
ref-0-id-234	lemma plusAssociativity(F)
ref-0-id-235	lemma plus0(F)
ref-0-id-236	lemma plusCommutativity(F)
ref-0-id-237	lemma timesAssociativity(F)
ref-0-id-238	lemma times1f
ref-0-id-239	lemma 2cauchy helper
ref-0-id-240	lemma 2cauchy
ref-0-id-241	lemma reciprocalF nonzero
ref-0-id-242	lemma eventually=f to sameF helper
ref-0-id-243	lemma eventually=f to sameF
ref-0-id-244	lemma fromNotSameF(Strong) helper2
ref-0-id-245	lemma fromNotSameF(Strong) helper
ref-0-id-246	lemma fromNotSameF(Strong)
ref-0-id-247	lemma sameFreciprocal helper
ref-0-id-248	lemma sameFreciprocal
ref-0-id-249	lemma from!!==
ref-0-id-250	lemma reciprocal(R)
ref-0-id-251	lemma timesCommutativity(F)
ref-0-id-252	lemma distribution(F)
ref-0-id-253	lemma fromMax(1)
ref-0-id-254	lemma fromMax(2)
ref-0-id-255	prop lemma to negated and
ref-0-id-256	lemma distributionOut
ref-0-id-257	lemma distributionOutLeft
ref-0-id-258	lemma distributionLeft
ref-0-id-259	lemma fromNotLess(R)
ref-0-id-260	lemma cartProdIsRelation
ref-0-id-261	lemma fromSubset
ref-0-id-262	lemma subsetIsRelation
ref-0-id-263	lemma toSeries
ref-0-id-264	lemma fromSeries
ref-0-id-265	lemma seriesSubsetCP
ref-0-id-266	lemma valueType
ref-0-id-267	prop lemma remove or
ref-0-id-268	lemma fromSingleton
ref-0-id-269	lemma inPair(1)
ref-0-id-270	lemma inPair(2)
ref-0-id-271	lemma sameMember(2)
ref-0-id-272	lemma toBinaryUnion(1)
ref-0-id-273	lemma toBinaryUnion(2)
ref-0-id-274	lemma fromOrderedPair(twoLevels)
ref-0-id-275	lemma toCartProd helper
ref-0-id-276	lemma toCartProd
ref-0-id-277	lemma nonreciprocalToRight(Eq)
ref-0-id-278	lemma nonreciprocalToLeft(Eq)(1 term)
ref-0-id-279	lemma sameReciprocal
ref-0-id-280	lemma CPseparationIsRelation
ref-0-id-281	lemma orderedPairEquality
ref-0-id-282	lemma reciprocalIsFunction
ref-0-id-283	lemma reciprocalIsTotal
ref-0-id-284	lemma reciprocalIsRationalSeries
ref-0-id-285	lemma crsIsRelation
ref-0-id-286	lemma crsIsFunction
ref-0-id-287	lemma crsIsTotal
ref-0-id-288	lemma crsIsSeries
ref-0-id-289	lemma crsLookup
ref-0-id-290	lemma 0f
ref-0-id-291	lemma 1f
ref-0-id-292	lemma toSingleton
ref-0-id-293	lemma fromSameSingleton
ref-0-id-294	lemma singletonmembersEqual
ref-0-id-295	lemma unequalsNotInSingleton
ref-0-id-296	lemma nonsingletonmembersUnequal
ref-0-id-297	lemma fromOrderedPair
ref-0-id-298	lemma fromOrderedPair(1)
ref-0-id-299	lemma fromOrderedPair(2)
ref-0-id-300	lemma fromCartProd
ref-0-id-301	lemma fromCartProd(1)
ref-0-id-302	lemma fromCartProd(2)
ref-0-id-303	lemma sameOrderedPair
ref-0-id-304	lemma inSeries helper
ref-0-id-305	lemma inSeries
ref-0-id-306	lemma to=f subset helper
ref-0-id-307	lemma to=f subset
ref-0-id-308	lemma to=f
ref-0-id-309	lemma productIsFunction
ref-0-id-310	lemma productIsTotal
ref-0-id-311	lemma productIsRationalSeries
ref-0-id-312	lemma timesF
ref-0-id-313	lemma -x+(1/2)x=-(1/2)x
ref-0-id-314	lemma positiveTripled
ref-0-id-315	lemma positiveDividedBy3
ref-0-id-316	lemma |x-x|=0
ref-0-id-317	lemma 1<2
ref-0-id-318	lemma 1/3<2/3
ref-0-id-319	lemma (1/3)x+(1/3)x=(2/3)x
ref-0-id-320	lemma (2/3)x+(1/3)x=x
ref-0-id-321	lemma -x+(2/3)x=-(1/3)x
ref-0-id-322	lemma -(1/3)x-(1/3)x=-(2/3)x
ref-0-id-323	lemma -x+(1/3)x=-(2/3)x
ref-0-id-324	lemma preserveLessGreater
ref-0-id-325	lemma closetolessIsLess
ref-0-id-326	lemma subLessLeft(F)
ref-0-id-327	lemma subLessLeft(R)
ref-0-id-328	lemma closetogreaterIsGreater
ref-0-id-329	lemma subLessRight(F)
ref-0-id-330	lemma subLessRight(R)
ref-0-id-331	lemma plus0Left
ref-0-id-332	lemma times1Left
ref-0-id-333	lemma eqAdditionLeft
ref-0-id-334	lemma eqMultiplicationLeft
ref-0-id-335	lemma plusF(Sym)
ref-0-id-336	lemma timesF(Sym)
ref-0-id-337	lemma sameSeries(Gen)
ref-0-id-338	lemma equalsSameF
ref-0-id-339	lemma leqReflexivity(R)
ref-0-id-340	tester1
ref-0-id-341	tester2
ref-0-id-342	tester3
ref-0-id-343	tester4
ref-0-id-344	tester5
ref-0-id-345	tester6