Volume 10, 1998

University of Bialystok

Copyright (c) 1998 Association of Mizar Users

### 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;

Back to top