[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
[mizar] 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 <adamn@math.uwb.edu.pl> 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
>>
>> trybulec@math.uwb.edu.pl 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 <jesse.alama@gmail.com>:
>>>
>>>> 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/