The abstract of the Mizar article:

The Properties of Product of Relational Structures

by

Artur Kornilowicz

Received March 27, 1998

MML identifier: YELLOW10

[ Mizar article, MML identifier index ]

environ

 vocabulary LATTICES, ORDERS_1, LATTICE3, RELAT_2, YELLOW_0, BOOLE, BHSP_3,
      ORDINAL2, FUNCT_5, MCART_1, WAYBEL_0, WAYBEL_3, QUANTAL1, COMPTS_1,
      WAYBEL_8, WAYBEL_6, WAYBEL11, WAYBEL_2;
 notation TARSKI, XBOOLE_0, ZFMISC_1, STRUCT_0, MCART_1, ORDERS_1, LATTICE3,
      YELLOW_0, WAYBEL_0, WAYBEL_1, YELLOW_3, YELLOW_4, WAYBEL_2, WAYBEL_3,
      WAYBEL_6, WAYBEL_8, WAYBEL11;
 constructors YELLOW_4, WAYBEL_1, WAYBEL_3, WAYBEL_6, WAYBEL_8, ORDERS_3,
      WAYBEL11;
 clusters STRUCT_0, LATTICE3, YELLOW_0, YELLOW_3, YELLOW_4, WAYBEL_0, WAYBEL_2,
      WAYBEL_3, WAYBEL_8, WAYBEL14, SUBSET_1, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin  :: On the elements of product of relational structures

definition let S, T be non empty upper-bounded RelStr;
 cluster [:S,T:] -> upper-bounded;
end;

definition let S, T be non empty lower-bounded RelStr;
 cluster [:S,T:] -> lower-bounded;
end;

theorem :: YELLOW10:1
  for S, T being non empty RelStr st [:S,T:] is upper-bounded
 holds S is upper-bounded & T is upper-bounded;

theorem :: YELLOW10:2
  for S, T being non empty RelStr st [:S,T:] is lower-bounded
 holds S is lower-bounded & T is lower-bounded;

theorem :: YELLOW10:3
for S, T being upper-bounded antisymmetric non empty RelStr holds
 Top [:S,T:] = [Top S,Top T];

theorem :: YELLOW10:4
for S, T being lower-bounded antisymmetric non empty RelStr holds
 Bottom [:S,T:] = [Bottom S,Bottom T];

theorem :: YELLOW10:5
for S, T being lower-bounded antisymmetric non empty RelStr,
    D being Subset of [:S,T:]
  st [:S,T:] is complete or ex_sup_of D,[:S,T:]
  holds sup D = [sup proj1 D,sup proj2 D];

theorem :: YELLOW10:6
  for S, T being upper-bounded antisymmetric (non empty RelStr),
    D being Subset of [:S,T:]
  st [:S,T:] is complete or ex_inf_of D,[:S,T:]
  holds inf D = [inf proj1 D,inf proj2 D];

theorem :: YELLOW10:7
  for S, T being non empty RelStr,
    x, y being Element of [:S,T:] holds
 x is_<=_than {y} iff x`1 is_<=_than {y`1} & x`2 is_<=_than {y`2};

theorem :: YELLOW10:8
  for S, T being non empty RelStr,
    x, y, z being Element of [:S,T:] holds
 x is_<=_than {y,z} iff x`1 is_<=_than {y`1,z`1} & x`2 is_<=_than {y`2,z`2};

theorem :: YELLOW10:9
  for S, T being non empty RelStr,
    x, y being Element of [:S,T:] holds
 x is_>=_than {y} iff x`1 is_>=_than {y`1} & x`2 is_>=_than {y`2};

theorem :: YELLOW10:10
  for S, T being non empty RelStr,
    x, y, z being Element of [:S,T:] holds
 x is_>=_than {y,z} iff x`1 is_>=_than {y`1,z`1} & x`2 is_>=_than {y`2,z`2};

theorem :: YELLOW10:11
  for S, T being non empty antisymmetric RelStr,
    x, y being Element of [:S,T:] holds
 ex_inf_of {x,y},[:S,T:] iff ex_inf_of {x`1,y`1}, S & ex_inf_of {x`2,y`2}, T;

theorem :: YELLOW10:12
  for S, T being non empty antisymmetric RelStr,
    x, y being Element of [:S,T:] holds
 ex_sup_of {x,y},[:S,T:] iff ex_sup_of {x`1,y`1}, S & ex_sup_of {x`2,y`2}, T;

theorem :: YELLOW10:13
for S, T being with_infima antisymmetric RelStr,
    x, y being Element of [:S,T:]
 holds (x "/\" y)`1 = x`1 "/\" y`1 & (x "/\" y)`2 = x`2 "/\" y`2;

theorem :: YELLOW10:14
for S, T being with_suprema antisymmetric RelStr,
    x, y being Element of [:S,T:]
 holds (x "\/" y)`1 = x`1 "\/" y`1 & (x "\/" y)`2 = x`2 "\/" y`2;

theorem :: YELLOW10:15
for S, T being with_infima antisymmetric RelStr,
    x1, y1 being Element of S,
    x2, y2 being Element of T
 holds [x1 "/\" y1, x2 "/\" y2] = [x1,x2] "/\" [y1,y2];

theorem :: YELLOW10:16
for S, T being with_suprema antisymmetric RelStr,
    x1, y1 being Element of S,
    x2, y2 being Element of T
 holds [x1 "\/" y1, x2 "\/" y2] = [x1,x2] "\/" [y1,y2];

definition let S be with_suprema with_infima antisymmetric RelStr,
               x, y be Element of S;
 redefine pred y is_a_complement_of x;
symmetry;
end;

theorem :: YELLOW10:17
for S, T being bounded with_suprema with_infima antisymmetric RelStr,
    x, y being Element of [:S,T:] holds
 x is_a_complement_of y iff
 x`1 is_a_complement_of y`1 & x`2 is_a_complement_of y`2;

theorem :: YELLOW10:18
for S, T being antisymmetric up-complete (non empty reflexive RelStr),
    a, c being Element of S, b, d being Element of T st [a,b] << [c,d]
 holds a << c & b << d;

theorem :: YELLOW10:19
for S, T being up-complete (non empty Poset)
 for a, c being Element of S, b, d being Element of T holds
  [a,b] << [c,d] iff a << c & b << d;

theorem :: YELLOW10:20
for S, T being antisymmetric up-complete (non empty reflexive RelStr),
    x, y being Element of [:S,T:] st x << y holds
  x`1 << y`1 & x`2 << y`2;

theorem :: YELLOW10:21
for S, T being up-complete (non empty Poset),
    x, y being Element of [:S,T:] holds
  x << y iff x`1 << y`1 & x`2 << y`2;

theorem :: YELLOW10:22
for S, T being antisymmetric up-complete (non empty reflexive RelStr),
    x being Element of [:S,T:]
 st x is compact holds x`1 is compact & x`2 is compact;

theorem :: YELLOW10:23
for S, T being up-complete (non empty Poset),
    x being Element of [:S,T:]
 st x`1 is compact & x`2 is compact holds x is compact;


begin  :: On the subsets of product of relational structures

theorem :: YELLOW10:24
for S, T being with_infima antisymmetric RelStr,
    X, Y being Subset of [:S,T:]
 holds proj1 (X "/\" Y) = proj1 X "/\" proj1 Y &
       proj2 (X "/\" Y) = proj2 X "/\" proj2 Y;

theorem :: YELLOW10:25
  for S, T being with_suprema antisymmetric RelStr,
    X, Y being Subset of [:S,T:]
 holds proj1 (X "\/" Y) = proj1 X "\/" proj1 Y &
       proj2 (X "\/" Y) = proj2 X "\/" proj2 Y;

theorem :: YELLOW10:26
  for S, T being RelStr, X being Subset of [:S,T:] holds
 downarrow X c= [:downarrow proj1 X,downarrow proj2 X:];

theorem :: YELLOW10:27
  for S, T being RelStr, X being Subset of S, Y being Subset of T holds
 [:downarrow X,downarrow Y:] = downarrow [:X,Y:];

theorem :: YELLOW10:28
for S, T being RelStr, X being Subset of [:S,T:] holds
 proj1 downarrow X c= downarrow proj1 X &
 proj2 downarrow X c= downarrow proj2 X;

theorem :: YELLOW10:29
  for S being RelStr, T being reflexive RelStr, X being Subset of [:S,T:] holds
 proj1 downarrow X = downarrow proj1 X;

theorem :: YELLOW10:30
  for S being reflexive RelStr, T being RelStr, X being Subset of [:S,T:] holds
 proj2 downarrow X = downarrow proj2 X;

theorem :: YELLOW10:31
  for S, T being RelStr, X being Subset of [:S,T:] holds
 uparrow X c= [:uparrow proj1 X,uparrow proj2 X:];

theorem :: YELLOW10:32
  for S, T being RelStr, X being Subset of S, Y being Subset of T holds
 [:uparrow X,uparrow Y:] = uparrow [:X,Y:];

theorem :: YELLOW10:33
for S, T being RelStr, X being Subset of [:S,T:] holds
 proj1 uparrow X c= uparrow proj1 X &
 proj2 uparrow X c= uparrow proj2 X;

theorem :: YELLOW10:34
  for S being RelStr, T being reflexive RelStr, X being Subset of [:S,T:] holds
 proj1 uparrow X = uparrow proj1 X;

theorem :: YELLOW10:35
  for S being reflexive RelStr, T being RelStr, X being Subset of [:S,T:] holds
 proj2 uparrow X = uparrow proj2 X;

theorem :: YELLOW10:36
  for S, T being non empty RelStr, s being Element of S, t being Element of T
 holds [:downarrow s,downarrow t:] = downarrow [s,t];

theorem :: YELLOW10:37
for S, T being non empty RelStr, x being Element of [:S,T:] holds
 proj1 downarrow x c= downarrow x`1 &
 proj2 downarrow x c= downarrow x`2;

theorem :: YELLOW10:38
  for S being non empty RelStr, T being non empty reflexive RelStr,
    x being Element of [:S,T:] holds
 proj1 downarrow x = downarrow x`1;

theorem :: YELLOW10:39
  for S being non empty reflexive RelStr, T being non empty RelStr,
    x being Element of [:S,T:] holds
 proj2 downarrow x = downarrow x`2;

theorem :: YELLOW10:40
  for S, T being non empty RelStr, s being Element of S, t being Element of T
 holds [:uparrow s,uparrow t:] = uparrow [s,t];

theorem :: YELLOW10:41
for S, T being non empty RelStr, x being Element of [:S,T:] holds
 proj1 uparrow x c= uparrow x`1 &
 proj2 uparrow x c= uparrow x`2;

theorem :: YELLOW10:42
  for S being non empty RelStr, T being non empty reflexive RelStr,
    x being Element of [:S,T:] holds
 proj1 uparrow x = uparrow x`1;

theorem :: YELLOW10:43
  for S being non empty reflexive RelStr, T being non empty RelStr,
    x being Element of [:S,T:] holds
 proj2 uparrow x = uparrow x`2;

theorem :: YELLOW10:44
for S, T being up-complete (non empty Poset),
    s being Element of S, t being Element of T
 holds [:waybelow s,waybelow t:] = waybelow [s,t];

theorem :: YELLOW10:45
for S, T being antisymmetric up-complete (non empty reflexive RelStr),
    x being Element of [:S,T:] holds
 proj1 waybelow x c= waybelow x`1 &
 proj2 waybelow x c= waybelow x`2;

theorem :: YELLOW10:46
for S being up-complete (non empty Poset),
    T being up-complete lower-bounded (non empty Poset),
    x being Element of [:S,T:] holds
 proj1 waybelow x = waybelow x`1;

theorem :: YELLOW10:47
for S being up-complete lower-bounded (non empty Poset),
    T being up-complete (non empty Poset),
    x being Element of [:S,T:] holds
 proj2 waybelow x = waybelow x`2;

theorem :: YELLOW10:48
  for S, T being up-complete (non empty Poset),
    s being Element of S, t being Element of T
 holds [:wayabove s,wayabove t:] = wayabove [s,t];

theorem :: YELLOW10:49
  for S, T being antisymmetric up-complete (non empty reflexive RelStr),
    x being Element of [:S,T:] holds
 proj1 wayabove x c= wayabove x`1 &
 proj2 wayabove x c= wayabove x`2;

theorem :: YELLOW10:50
for S, T being up-complete (non empty Poset),
    s being Element of S, t being Element of T
 holds [:compactbelow s,compactbelow t:] = compactbelow [s,t];

theorem :: YELLOW10:51
for S, T being antisymmetric up-complete (non empty reflexive RelStr),
    x being Element of [:S,T:] holds
 proj1 compactbelow x c= compactbelow x`1 &
 proj2 compactbelow x c= compactbelow x`2;

theorem :: YELLOW10:52
for S being up-complete (non empty Poset),
    T being up-complete lower-bounded (non empty Poset),
    x being Element of [:S,T:] holds
 proj1 compactbelow x = compactbelow x`1;

theorem :: YELLOW10:53
for S being up-complete lower-bounded (non empty Poset),
    T being up-complete (non empty Poset),
    x being Element of [:S,T:] holds
 proj2 compactbelow x = compactbelow x`2;

definition let S be non empty reflexive RelStr;
 cluster empty -> Open Subset of S;
end;

theorem :: YELLOW10:54
  for S, T being antisymmetric up-complete (non empty reflexive RelStr),
    X being Subset of [:S,T:] st
 X is Open holds proj1 X is Open & proj2 X is Open;

theorem :: YELLOW10:55
  for S, T being up-complete (non empty Poset),
    X being Subset of S, Y being Subset of T st X is Open & Y is Open
 holds [:X,Y:] is Open;

theorem :: YELLOW10:56
  for S, T being antisymmetric up-complete (non empty reflexive RelStr),
    X being Subset of [:S,T:] st
 X is inaccessible holds proj1 X is inaccessible & proj2 X is inaccessible;

theorem :: YELLOW10:57
  for S, T being antisymmetric up-complete (non empty reflexive RelStr),
    X being upper Subset of S, Y being upper Subset of T st
  X is inaccessible & Y is inaccessible holds [:X,Y:] is inaccessible;

theorem :: YELLOW10:58
  for S, T being antisymmetric up-complete (non empty reflexive RelStr),
    X being Subset of S, Y being Subset of T st [:X,Y:] is directly_closed
 holds (Y <> {} implies X is directly_closed) &
       (X <> {} implies Y is directly_closed);

theorem :: YELLOW10:59
  for S, T being antisymmetric up-complete (non empty reflexive RelStr),
    X being Subset of S, Y being Subset of T
  st X is directly_closed & Y is directly_closed
 holds [:X,Y:] is directly_closed;

theorem :: YELLOW10:60
  for S, T being antisymmetric up-complete (non empty reflexive RelStr),
    X being Subset of [:S,T:] st X has_the_property_(S) holds
 proj1 X has_the_property_(S) & proj2 X has_the_property_(S);

theorem :: YELLOW10:61
  for S, T being up-complete (non empty Poset),
    X being Subset of S, Y being Subset of T
  st X has_the_property_(S) & Y has_the_property_(S)
 holds [:X,Y:] has_the_property_(S);


begin  :: On the products of relational structures

theorem :: YELLOW10:62
for S, T being non empty reflexive RelStr
 st the RelStr of S = the RelStr of T & S is /\-complete
   holds T is /\-complete;

definition let S be /\-complete (non empty reflexive RelStr);
 cluster the RelStr of S -> /\-complete;
end;

definition let S, T be /\-complete (non empty reflexive RelStr);
 cluster [:S,T:] -> /\-complete;
end;

theorem :: YELLOW10:63
  for S, T being non empty reflexive RelStr st [:S,T:] is /\-complete
 holds S is /\-complete & T is /\-complete;

definition let S, T be complemented bounded with_infima with_suprema
                       antisymmetric (non empty RelStr);
 cluster [:S,T:] -> complemented;
end;

theorem :: YELLOW10:64
  for S, T being bounded with_infima with_suprema antisymmetric RelStr
 st [:S,T:] is complemented holds S is complemented & T is complemented;

definition let S, T be distributive with_infima with_suprema antisymmetric
                       (non empty RelStr);
 cluster [:S,T:] -> distributive;
end;

theorem :: YELLOW10:65
  for S being with_infima with_suprema antisymmetric RelStr,
    T being with_infima with_suprema reflexive antisymmetric RelStr
 st [:S,T:] is distributive holds S is distributive;

theorem :: YELLOW10:66
  for S being with_infima with_suprema reflexive antisymmetric RelStr,
    T being with_infima with_suprema antisymmetric RelStr
 st [:S,T:] is distributive holds T is distributive;

definition let S, T be meet-continuous Semilattice;
 cluster [:S,T:] -> satisfying_MC;
end;

theorem :: YELLOW10:67
  for S, T being Semilattice st [:S,T:] is meet-continuous holds
 S is meet-continuous & T is meet-continuous;

definition let S, T be satisfying_axiom_of_approximation up-complete
                       /\-complete (non empty Poset);
 cluster [:S,T:] -> satisfying_axiom_of_approximation;
end;

definition let S, T be continuous /\-complete (non empty Poset);
 cluster [:S,T:] -> continuous;
end;

theorem :: YELLOW10:68
  for S, T being up-complete lower-bounded (non empty Poset)
 st [:S,T:] is continuous holds S is continuous & T is continuous;

definition let S, T be satisfying_axiom_K up-complete lower-bounded
                       sup-Semilattice;
 cluster [:S,T:] -> satisfying_axiom_K;
end;

definition let S, T be complete algebraic lower-bounded sup-Semilattice;
 cluster [:S,T:] -> algebraic;
end;

theorem :: YELLOW10:69
for S, T being lower-bounded (non empty Poset)
 st [:S,T:] is algebraic holds S is algebraic & T is algebraic;

definition let S, T be arithmetic lower-bounded LATTICE;
 cluster [:S,T:] -> arithmetic;
end;

theorem :: YELLOW10:70
  for S, T being lower-bounded LATTICE st [:S,T:] is arithmetic holds
 S is arithmetic & T is arithmetic;