[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] the carrier of and [#]

On Wed, 4 Apr 2007, Jesse Alama wrote:


I faced a surprising problem recently concerning a seeming lack of
equality of

 [#]V

and

 the carrier of V,

where V has type VectSp of F, and F has type Field.  Specifically, the
statement

 consider G being FinSequence of [#]V such that
   G is one-to-one and
   rng G = Carrier l and
   x - y = Sum (l (#) G) by VECTSP_6:def 9;
::>                  *103

where l is type Linear_Combination of A, A has type Subset of V, and x
and y have type Element of V, is rejected.  For reference,
VECTSP_6:def 9 is

 definition let GF be non empty LoopStr;
            let V be non empty VectSpStr over GF;
            let L be Linear_Combination of V;
  assume A1: V is Abelian add-associative right_zeroed right_complementable;
  func Sum(L) -> Element of V means
   :Def9: ex F being FinSequence of the carrier of V st
     F is one-to-one & rng F = Carrier(L) & it = Sum(L (#) F);

However, by changing "[#]V" to "the carrier of V", my statement is
accepted.  This surprised me, since, according to STRUCT_0:def 3, we
have [#]V = the carrier of V, and my original statement is rejected
even if I cite STRUCT_0:def 3.  What might be going on?
Is STRUCT_0 listed in the 'definitions' directive? - only then the 'equals' definition works automatically - adding a subsequent reference to a universal sentence (the definitional theorem of STRUCT_0:def 3) won't help since the checker is able to use only one such universal premise in one disjunct in an inference. 

Best,
Adam Naumowicz

======================================================================
Department of Applied Logic            fax. +48 (85) 745-7662
Institute of Computer Science          tel. +48 (85) 745-7559 (office)
University of Bialystok                e-mail: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland   http://math.uwb.edu.pl/~adamn/
======================================================================