The abstract of the Mizar article:

The Correspondence Between Lattices of Subalgebras of Universal Algebras and Many Sorted Algebras

by

Adam Naumowicz, and

Agnieszka Julia Marasik

Received September 22, 1998

MML identifier: MSSUBLAT

[ Mizar article, MML identifier index ]

environ

 vocabulary MSUALG_1, FUNCT_1, BOOLE, FINSEQ_2, FINSEQ_1, RELAT_1, FUNCOP_1,
      UNIALG_1, UNIALG_2, CQC_SIM1, PRALG_1, MSUALG_2, TDGROUP, QC_LANG1,
      PARTFUN1, FINSEQ_4, ZF_REFLE, AMI_1, PBOOLE, CARD_3, FUNCT_2, REALSET1,
      CAT_1, LATTICES, INCPROJ, WELLORD1, GROUP_6;
 notation TARSKI, XBOOLE_0, SUBSET_1, BINOP_1, CARD_3, NAT_1, CQC_LANG,
      LATTICES, LATTICE4, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, STRUCT_0,
      PBOOLE, UNIALG_1, UNIALG_2, REALSET1, PRALG_1, NUMBERS, FINSEQ_1,
      FINSEQ_2, MSUALG_1, MSUALG_2;
 constructors BINOP_1, CQC_LANG, LATTICE4, ALG_1, MSUALG_2, PRALG_1, FINSEQOP,
      FILTER_1, MEMBERED;
 clusters FUNCT_1, MSUALG_1, MSUALG_2, RELSET_1, PRALG_1, STRUCT_0, UNIALG_1,
      UNIALG_2, FINSEQ_2, MSAFREE, CQC_LANG, ARYTM_3, XBOOLE_0, MEMBERED,
      NUMBERS, ORDINAL2, SUBSET_1;
 requirements NUMERALS, SUBSET, BOOLE;


begin

:: Preliminaries

reserve a for set, i for Nat;

theorem :: MSSUBLAT:1
 (*-->a).0 = {};

theorem :: MSSUBLAT:2
   (*-->a).1 = <*a*>;

theorem :: MSSUBLAT:3
   (*-->a).2 = <*a,a*>;

theorem :: MSSUBLAT:4
   (*-->a).3 = <*a,a,a*>;

theorem :: MSSUBLAT:5
 for f being FinSequence of {0} holds
  f = i |-> 0 iff len f = i;

theorem :: MSSUBLAT:6
 for f be FinSequence st f = (*-->0).i holds len f = i;

begin

:: Some Properties of Subalgebras of Universal and Many Sorted Algebras

theorem :: MSSUBLAT:7
 for U1,U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds
  MSSign U1 = MSSign U2;

definition
let U0 be Universal_Algebra;
cluster the charact of U0 -> Function-yielding;
end;

theorem :: MSSUBLAT:8
 for U1,U2 being Universal_Algebra st U1 is SubAlgebra of U2
  for B being MSSubset of MSAlg U2 st B = the Sorts of MSAlg U1
   for o being OperSymbol of MSSign U2
    for a being OperSymbol of MSSign U1 st a = o holds
     Den(a,MSAlg U1) = Den(o,MSAlg U2)|Args(a,MSAlg U1);

theorem :: MSSUBLAT:9
 for U1,U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds
  the Sorts of MSAlg U1 is MSSubset of MSAlg U2;

theorem :: MSSUBLAT:10
 for U1,U2 being Universal_Algebra st U1 is SubAlgebra of U2
  for B being MSSubset of MSAlg U2 st B = the Sorts of MSAlg U1 holds
   B is opers_closed;

theorem :: MSSUBLAT:11
 for U1,U2 being Universal_Algebra st U1 is SubAlgebra of U2
  for B being MSSubset of MSAlg U2 st B = the Sorts of MSAlg U1 holds
   the Charact of MSAlg U1 = Opers(MSAlg U2,B);

theorem :: MSSUBLAT:12
 for U1,U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds
  MSAlg U1 is MSSubAlgebra of MSAlg U2;

theorem :: MSSUBLAT:13
 for U1,U2 being Universal_Algebra st MSAlg U1 is MSSubAlgebra of MSAlg U2
  holds the carrier of U1 is Subset of U2;

theorem :: MSSUBLAT:14
 for U1,U2 being Universal_Algebra st MSAlg U1 is MSSubAlgebra of MSAlg U2
  for B being non empty Subset of U2
   st B=the carrier of U1 holds B is opers_closed;

theorem :: MSSUBLAT:15
 for U1,U2 being Universal_Algebra st MSAlg U1 is MSSubAlgebra of MSAlg U2
  for B being non empty Subset of U2
   st B=the carrier of U1 holds the charact of U1 = Opers(U2,B);

theorem :: MSSUBLAT:16
 for U1,U2 being Universal_Algebra st MSAlg U1 is MSSubAlgebra of MSAlg U2
  holds U1 is SubAlgebra of U2;

reserve MS for segmental trivial non void non empty ManySortedSign,
        A for non-empty MSAlgebra over MS;

theorem :: MSSUBLAT:17
 for B being non-empty MSSubAlgebra of A holds
  the carrier of 1-Alg B is Subset of 1-Alg A;

theorem :: MSSUBLAT:18
 for B being non-empty MSSubAlgebra of A holds
  for S being non empty Subset of 1-Alg A st
   S = the carrier of 1-Alg B holds S is opers_closed;

theorem :: MSSUBLAT:19
 for B being non-empty MSSubAlgebra of A holds
  for S being non empty Subset of 1-Alg A st
   S = the carrier of 1-Alg B holds
    the charact of(1-Alg B) = Opers(1-Alg A,S);

theorem :: MSSUBLAT:20
 for B being non-empty MSSubAlgebra of A holds
  1-Alg B is SubAlgebra of 1-Alg A;

theorem :: MSSUBLAT:21
 for S being non empty non void ManySortedSign,
  A,B being MSAlgebra over S holds
   A is MSSubAlgebra of B iff A is MSSubAlgebra of the MSAlgebra of B;

theorem :: MSSUBLAT:22
   for A,B being Universal_Algebra holds
  signature A = signature B iff MSSign A = MSSign B;

theorem :: MSSUBLAT:23
 for A being non-empty MSAlgebra over MS st the carrier of MS = {0}
  holds MSSign 1-Alg A = the ManySortedSign of MS;

theorem :: MSSUBLAT:24
 for A,B being non-empty MSAlgebra over MS
  st the carrier of MS ={0} & 1-Alg A = 1-Alg B
   holds the MSAlgebra of A = the MSAlgebra of B;

theorem :: MSSUBLAT:25
   for A being non-empty MSAlgebra over MS st the carrier of MS = {0} holds
  the Sorts of A = the Sorts of MSAlg (1-Alg A);

theorem :: MSSUBLAT:26
 for A being non-empty MSAlgebra over MS st the carrier of MS = {0}
  holds MSAlg (1-Alg A) = the MSAlgebra of A;

theorem :: MSSUBLAT:27
   for A being Universal_Algebra,
  B being strict non-empty MSSubAlgebra of MSAlg A
   st the carrier of MSSign A = {0}
    holds 1-Alg B is SubAlgebra of A;

begin

::  The Correspondence Between Lattices of Subalgebras of
::  Universal and Many Sorted Algebras

theorem :: MSSUBLAT:28
 for A being Universal_Algebra,
  a1,b1 being strict non-empty SubAlgebra of A,
   a2,b2 being strict non-empty
    MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1
     holds (the Sorts of a2) \/ (the Sorts of b2) =
      0 .--> ((the carrier of a1) \/ (the carrier of b1));

theorem :: MSSUBLAT:29
 for A being Universal_Algebra,
  a1,b1 being strict non-empty SubAlgebra of A,
   a2,b2 being strict non-empty
    MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1
     holds (the Sorts of a2) /\ (the Sorts of b2) =
      0 .--> ((the carrier of a1) /\ (the carrier of b1));

theorem :: MSSUBLAT:30
 for A being strict Universal_Algebra,
  a1,b1 be strict non-empty SubAlgebra of A,
   a2,b2 being strict non-empty MSSubAlgebra of MSAlg A
    st a2 = MSAlg a1 & b2 = MSAlg b1
     holds MSAlg (a1 "\/" b1) = a2 "\/" b2;

definition
let A be with_const_op Universal_Algebra;
cluster MSSign(A) -> non void strict segmental trivial all-with_const_op;
end;

theorem :: MSSUBLAT:31
 for A being with_const_op Universal_Algebra,
  a1,b1 being strict non-empty SubAlgebra of A,
   a2,b2 being strict non-empty MSSubAlgebra of MSAlg A
    st a2 = MSAlg a1 & b2 = MSAlg b1
     holds MSAlg (a1 /\ b1) = a2 /\ b2;

definition let A be quasi_total UAStr;
cluster the UAStr of A -> quasi_total;
end;

definition let A be partial UAStr;
cluster the UAStr of A -> partial;
end;

definition let A be non-empty UAStr;
cluster the UAStr of A -> non-empty;
end;

definition let A be with_const_op Universal_Algebra;
cluster the UAStr of A -> with_const_op;
end;

theorem :: MSSUBLAT:32
   for A being with_const_op Universal_Algebra holds
  UnSubAlLattice the UAStr of A, MSSubAlLattice MSAlg the UAStr of A
   are_isomorphic;