[mizar] Re: Lm9 of xcmplx_1

[Jesse Alama <jesse.alama@gmail.com>]

Hi Andrzej,

At

  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/