Revisions 1-5

Revision 1

The aim of this revision was to check if the changes in the article BOOLE will cause any changes in the tree of dependence of Mizar articles. The theorems which proof is straightforward justification ( 'by' another theorem, mainly definitional one in this case ) are no longer in BOOLE.MIZ. In place of such a theorem 'canceled' have been inserted.

From this version of MML using for example BOOLE:8 will cause 'Inaccessible theorem' error. In this case one should use BOOLE:def 2. Complete list of such changes is given below.

Every occurrence of canceled theorem in MML has been replaced in accordance with this list. It caused changes in 380 articles.

Finally, the compression of multiple 'canceled' has been done.

Adam Grabowski adamgrab@math.uw.bialystok.pl

Revision 2

The main goal of the revision was to eliminate overloading of the mode symbol "Finite_Subset". It was used twice:

in FINSUB_1 to introduce an expandable mode

  mode Finite_Subset of A is Element of Fin A

where A is an arbitrary set, and Fin A the set of all finite subsets of A

and in RLVECT_2 to introduce another mode ( RLVECT_2: def 2 ):

definition let V be 1-sorted;
 mode Finite_Subset of V -> Subset of the carrier of V means
   it is finite;
end;

definition let S be 1-sorted;
 mode Subset of S -> Subset of the carrier of S means
  not contradiction;
end;

1. The definition RLVECT_2 has been canceled, all occurrences of "Finite_Subset" have been changed to "finite Subset" and all references to the definitional theorem have been changed to STRUCT_0:def 3.
2. Cluster

   definition let V be 1-sorted;
    cluster empty finite Subset of V;
    existence
     proof ø is Subset of the carrier of V by SUBSET_1:4;
        then ø is Subset of V & ø is finite by STRUCT_0:def 3;
      hence thesis;
     end;
   end;

   has been inserted (the proof of existence borrowed from RLVECT_2:def 3)
3. Cluster

   definition let V be 1-sorted;
    cluster -> finite Finite_Subset of V;
    coherence by Def2;
   end;

   has been removed.

RLVECT_3, VECTSP_6, VECTSP_7, LMOD_5, RMOD_4, RMOD_5, MOD_3,
MATRLIN, VECTSP_9, RLVECT_5

for f being standard (non empty FinSequence of TOP-REAL 2) st k  dom f
 ex i,j st [i,j]  Indices GoB f & (f,k) = (GoB f)*(i,j);

for f being non empty FinSequence of TOP-REAL 2 st k  dom f
 ex i,j st [i,j]  Indices GoB f & (f,k) = (GoB f)*(i,j)

 (L~f)` <> ø;

Revision 3

The obvious consequences of the definitional theorems in articles VECTSP_1 and VECTSP_2 have been removed.

During one of old revisions Seg len p was automatically substituted by dom p but resulting conjuctions (disjunctions) of the form p & p (p or p) were not simplified. We did it in the case of these two theorems and they became equal to TOPREAL3:14 and GOBOARD1:11 respectively so the latter ones were canceled.

Instead of GOBOARD1:11 refer to GROUP_5:96
Instead of TOPREAL3:14 refer to GROUP_5:95

Instead of RELAT_1:59 refer to BOOLE:27
Instead of RELAT_1:58 refer to BOOLE:27
Instead of RELAT_1:61 refer to BOOLE:60 or BOOLE:61

Cancellations in RELAT_1 are long overdue and quite obvious.

theorem :: TOPS_2:58
 for T, S, V being non empty TopStruct
  for f being map of T,S, g being map of S,V st
   f is continuous & g is continuous holds gf is continuous;

The mother type of two functors in TOPREAL1:
  def 5 (of line segment) and
  def 6 (of a special polygonal arc) have been changed to Subset of TOP-REAL n (the original type: Subset of the carrier of TOP-REAL n).

Some of the theorems and definitions in ALTCAT_3 were generalized so in definitions 7, 8 and 12 loci "category" were replaced by "non empty AltCatStr" and in 9, 10, 11 - by "AltGraph", corresponding theorems were also strenghtened. Theorems 9, 10, 11 and 12 were generalized for associative transitive (non empty AltCatStr) and 1 - for "with_units (non empty AltCatStr)".

One existential registration of cluster was added:

definition
let C be with_units (non empty AltCatStr),
    o be object of C;
cluster mono epi retraction coretraction Morphism of o,o;
end;

For the changes in ALTCAT series thanks are due to Artur Kornilowicz.

Revision 4

definition
 let D be non empty set;
 let D1 be non empty Subset of D;
 let D2 be non empty Subset of D1;
 redefine mode Element of D2 ->Element of D1;
end;

definition let D be non empty set;
 let S be non empty Subset of D;
 redefine mode Element of S -> Element of D;
end;

for C being non empty AltCatStr, a1,a2,a3 being object of C
  st <^a1,a3^> = ø implies <^a1,a2^> = ø or <^a2,a3^> = ø
   holds (the Comp of C).(a1,a2,a3)
     is Function of [:<^a2,a3^>,<^a1,a2^>:],<^a1,a3^>;

<^a1,a3^> = ø implies <^a1,a2^> = ø or <^a2,a3^> = ø

definition let I1 be set,
 f,g be ManySortedFunction of I1;
 redefine func gf -> ManySortedFunction of I1;
end;

definition
  let A,B being category;
 cluster covariant -> Covariant feasible Functor of A,B;
end;

definition let A be transitive with_units (non empty AltCatStr),
               B be with_units (non empty AltCatStr);
 cluster -> feasible id-preserving Functor of A, B;
end;

definition let A be transitive with_units (non empty AltCatStr),
               B be with_units (non empty AltCatStr);
 cluster covariant -> Covariant comp-preserving Functor of A, B;
 cluster Covariant comp-preserving -> covariant Functor of A, B;
 cluster contravariant -> Contravariant comp-reversing Functor of A, B;
 cluster Contravariant comp-reversing -> contravariant Functor of A, B;
end;

definition
let L being non empty RelStr,
    X being Subset of L;
attr X is order-generating means
:: WAYBEL_6: def 5
for x be Element of L holds
 ex_inf_of (uparrow x)  X,L & x = inf ((uparrow x)  X);
end;

attr X is order-generating means
for x be Element of L holds x = inf ((uparrow x)  X);

C. The definition of expandable modes Nat and Real have been moved from ARYTM to NAT_1 and REAL_1, respectively. Because of this change it was necessary to add NAT_1 and REAL_1 to the notation directive in some articles.

Revision 5

definition let M,S1,n;
 redefine func S1.n -> Element of the carrier of M;
end;

definition let G be Group;let a be Element of the carrier of G;
 redefine func {a} -> Subset of the carrier of G;
end;

definition let G be Group; let a be Element of the carrier of G;
 redefine func {a} -> Subset of G;
end;

definition let n,k be Nat;
 redefine func max(n,k) -> Nat;
end;

definition
 let T be TopStruct, A be Subset of the carrier of T;
 redefine func Cl A -> Subset of T;
end;

definition let AS,X,Y;
  redefine func X ï Y -> Subset of the carrier of AS;
end;

definition
  let J be set, S be non empty 1-sorted;
  let F be Function of J, the carrier of S;
  redefine func rng F -> Subset of S;
end;

definition let A be set; let X be set;
 redefine func A --> X -> ManySortedSet of A;
end;

 A c= B iff succ A c= succ B;

theorem :: TOPS_1:2
  P U ê TS = ê TS & ê TS U P = ê TS;

theorem :: CARD_2:20
  0' = í & 0' = í & 1' = one;

theorem :: RCOMP_1:14
p=g implies [.p,g.] = {p} & [.g,p.] = {p} & ].p,g.[ = í;

 a=a+(b-b) & a=a+b-b & a=a+(b+-b) & a=a+b+-b
  & a=a-(b-b) & a=a-(b+-b) & a=a+-b+b
  & a=b-(b-a) & a=-b-(-a-b) & a=-b-(-b-a);

theorem :: REAL_2:88
 2ùa=a+a & 3ùa=a+a+a & 4ùa=a+a+a+a;

theorem :: INT_1:3
  r1 = (- r2 + r1) + r2 & r1 = r2 + (- r2 + r1) &
  r1 = r2 + (r1 - r2) & r1 = r2 + r1 - r2;

theorem :: CARD_5:4
 í = 0 & one = 1;

theorem :: CARD_5:7
 NAT = omega & NAT = alef 0;

theorem :: SCMFSA_7:11
 for p being FinSequence, i being Nat holds
     i î dom p iff 1 ó i & i ó len p;

for R being Relation, p being RedSequence of R holds
  1 î dom p & len p î dom p;

definition let A be set; let X be non empty set;
 cluster A --> X -> non-empty;
end;

definition
 let X be non empty set;
 cluster finite non empty Subset of X;
end;

definition
 let D,E be non empty set;
 cluster non empty Relation of D,E;
end;

definition
 let S be non empty non void ManySortedSign;
 let A be non-empty MSAlgebra over S;
 let o be OperSymbol of S;
 cluster -> FinSequence-like Element of Args(o,A);
end;

definition
 let X be non empty set;
 cluster -> non empty a_partition of X;
end;

 cluster empty -> Relation-like set;

  cluster strict non empty ÀÙ-SemiLattStr;
  cluster strict non empty Ú¿-SemiLattStr;

theorem :: NORMFORM:15
 a U b = b U a;
theorem :: NORMFORM:18
 a ï b = b ï a;

definition let A be set;
 cluster FinPairUnion A -> commutative idempotent associative;
end;

definition let A;
 func NormForm A -> strict LattStr means
:: NORMFORM: def 14
  the carrier of it = Normal_forms_on A &
  for B, C being Element of Normal_forms_on A holds
    (the L_join of it).(B, C) = mi (B U C) &
    (the L_meet of it).(B, C) = mi (B^C);
 end;

definition let A;
 func NormForm A -> strict 0_Lattice equals
  LattStr(#Normal_forms_on A, Join A, Meet A#);
 end;

definition let A;
  cluster NormForm A -> non empty;
  cluster NormForm A -> Lattice-like;
  cluster NormForm A -> distributive lower-bounded;
end;

definition let A;
  cluster NormForm A -> implicative;
end;

theorem :: NATTRA_1:18
 F is_transformable_to F;

theorem :: NATTRA_1:24
 F is_naturally_transformable_to F;

theorem :: NATTRA_1:29
 F ~= F;

theorem :: MSUALG_3:16
for U1 being non-empty MSAlgebra over S holds U1,U1 are_isomorphic;

definition let K,V;
 func ‡V -> non empty Subset of V equals
:: LMOD_6: def 4
  the carrier of V;
end;

definition let i,n;
  func Repeat(i,n) -> FinSequence of NAT means
:: GOBRD10: def 3
   len it =n & for j st 1ój & jón holds it.j=i;
end;

definition let n, i;
  redefine func n |-> i -> FinSequence of NAT means
:: GOBRD10: def 3
    len it = n & for j st 1 ó j & j ó n holds it.j = i;
end;

theorem :: REWRITE1:37
 for R being Relation, a,b being set st R reduces a,b
  holds a,b are_convergent_wrt R & a,b are_divergent_wrt R &
        b,a are_convergent_wrt R & b,a are_divergent_wrt R;