Re: Lm9 of xcmplx_1

Hi Adam,

Thanks; that's exactly what I'm looking for.

The next question is why the same theorem appears twice in the same
article, one time as an unexported lemma and then later as a proper
(exported) theorem.  Once I saw Lm9, I didn't search any further in
the article on the assumption that it wouldn't literally reappear
later.

Jesse

Adam Naumowicz <[email protected]> writes:

> Look here:
>
> theorem :: XCMPLX_1:89
> for b, a being complex number st b <> 0 holds
> a = (a * b) / b by Lm9;
>
> Best,
>
> Adam
>
> On Sun, 18 Mar 2012, Jesse Alama wrote:
>
>>  http://www.mizar.org/version/current/html/xcmplx_1.html#E62
>>
>> you can see that the theorem I have in mind is called Lm9 and it is
>> unexported.  I see this also in the .miz file for the official release
>> of MML 4.181.1147.  Do you see this as well?  In xreal_1.abs I see
>>
>> :: [ xreal_1.abs ] ::::::::::::::::::::::::::::::::::::::::::::::::::::
>>
>> :: snip
>>
>> theorem :: XCMPLX_1:53 :: REAL_2'31
>>  c <> 0 & a / c = b / c implies a = b;
>>
>> theorem :: XCMPLX_1:54 :: REAL_2'74
>>  a / b <> 0 implies b = a / (a / b);
>>
>> :: snip
>>
>> ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
>>
>> with no such lemma (as expected, since it is not exported).
>>
>> Jesse
>>
>> [email protected] writes:
>>
>>> Is it Lm9? I have
>>>
>>> Lm9: b<>0 implies a=a*b/b
>>>
>>> and it seems that it is so for long time.
>>>
>>> Anyway, you need the theorem
>>>
>>> theorem :: XCMPLX_1:52  a <> 0 implies a / (a / b) = b;
>>>
>>> Maybe in version that you use it has a different number.
>>>
>>> Lemmas are often proved because the order in which we prove and the
>>> order in which we
>>> want to list theorems in abstract are different. Then they are
>>> repeated as theorems with the justification "by lemma".
>>>
>>> I have checked lemmas in XCMPLX_1. All are exported as theorems:
>>>
>>> theorem :: REAL_1'24
>>>  a" * b" = (a * b)" by Lm1;
>>> theorem :: REAL_1'42
>>>  a / (b / c) = (a * c) / b by Lm2;
>>> theorem :: REAL_1'43
>>>  b <> 0 implies a / b * b = a by Lm3;
>>> theorem :: REAL_1'33_1
>>>  1 / a = a" by Lm4;
>>> theorem :: REAL_1'37
>>>  a <> 0 implies a / a = 1 by Lm5;
>>> theorem :: REAL_1'35
>>>  (a / b) * (c / d) = (a * c) / (b * d) by Lm6;
>>> theorem :: REAL_1'81
>>>  (a / b)" = b / a by Lm7;
>>> theorem :: SQUARE_1'18
>>>  a * (b / c) = (a * b) / c by Lm8;
>>> theorem :: REAL_2'62_2
>>>  b <> 0 implies a = a * b / b by Lm9;
>>> theorem :: REAL_1'38
>>>  c <> 0 implies a / b = (a * c) / (b * c) by Lm10;
>>> theorem :: REAL_2'47_1
>>>   (a * b")" = a" * b by Lm11;
>>> theorem :: REAL_2'33_1
>>>  a" = b" implies a = b by Lm12;
>>> theorem :: REAL_1'82
>>>  (a / b) / (c / d) = (a * d) / (b * c) by Lm13;
>>> theorem :: REAL_2'56:
>>>  a * (1 / b) = a / b by Lm14;
>>> theorem :: REAL_2'67_4
>>>  1 / c * (a / b) = a / (b * c) by Lm15;
>>> theorem :: REAL_1'33_2
>>>  1 / a" = a by Lm16;
>>> theorem :: REAL_1'39_1
>>>  -a / b = (-a) / b by Lm17;
>>> theorem :: REAL_2'46_1
>>>  a <> 0 & a = a" implies a = 1 or a = -1 by Lm18;
>>> theorem :: REAL_2'45_1
>>>  (- a)" = -a" by Lm19;
>>>
>>> Greetings,
>>> Andrzej
>>>
>>>
>>> Cytowanie Jesse Alama <[email protected]>:
>>>
>>>> Please promote Lm9 of XCMPLX_1 (MML 4.181.1147)
>>>>
>>>> for a, b being complex number
>>>>  st a <> 0 holds
>>>>  a / (a / b) = b
>>>>
>>>> to a proper theorem.  It is quite silly to repeat the proof of this
>>>> fact in an article.
>>>>
>>>> Imagine if a mathematician stated and proved this lemma in a paper on
>>>> advanced complex analysis, with an apology: "The author of this useful
>>>> lemma forbade me from citing it, so I have to reinvent this little
>>>> wheel.  Let a and b be complex numbers, and assume that a is
>>>> nonzero. ..."
>>>>
>>>> In fact, why not promote *all* the lemmas of XCMPLX_1 to proper
>>>> theorems?  In this kind of article (part of the Encyclopedia), its many
>>>> lemmas might be useful in many contexts.  No private lemmas, please!
>>>>
>>>> More generally, I am not convinced of the value of unexported
>>>> theorems.  Neither an author nor the MML Library Committee knows just
>>>> when a lemma might be useful for other people in contexts they don't
>>>> currently work with.  Sure, in the course of writing an article (or
>>>> maintaining it in light of other changes to the library), it might
>>>> feel right to "hide" a lemma because it seems, at the time of writing,
>>>> too specialized and therefore likely to have little reuse value to
>>>> other authors.  And for the purposes of a JFM version of an article,
>>>> maybe it is reasonable to suppress some excessively
>>>> specialized/customized lemmas.  But with a growing MML, and greater
>>>> reuse of more and more of its articles, I fail to see the value in
>>>> hiding anything at all.  Expose all theorems and let the community of
>>>> users of the MML, not the author of a particular article, decide which
>>>> lemmas are important.
>>>>
>>>> Even if one disagrees with this general view of unexported theorems, I
>>>> still think that for articles like XCMPLX_1, which are supposed to lay
>>>> out a large variety of useful theorems, I fail to see the value in
>>>> keeping any theorem private (unexported).
>>>>
>>>> Jesse
>>>>
>>>> --
>>>> Jesse Alama
>>>> http://centria.di.fct.unl.pt/~alama/
>>>>
>>>
>>>
>>>
>>
>> -- 
>> Jesse Alama
>> http://centria.di.fct.unl.pt/~alama/
>>
>
>

-- 
Jesse Alama
http://centria.di.fct.unl.pt/~alama/