:: More on the Lattice of Many Sorted Equivalence Relations
:: by Robert Milewski
::
:: Received February 9, 1996
:: Copyright (c) 1996-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, PBOOLE, REAL_1, STRUCT_0, MSUALG_5, EQREL_1,
RELAT_1, FUNCT_1, MSUALG_4, TARSKI, ZFMISC_1, XXREAL_2, SUBSET_1,
LATTICES, CLOSURE2, SETFAM_1, FUNCT_4, REWRITE1, LATTICE3, MSSUBFAM,
NAT_LAT, REALSET1, XXREAL_0, XXREAL_1, REAL_LAT, BINOP_1, SUPINF_1,
ORDINAL2, ARYTM_1, CARD_1, ARYTM_3, MSUALG_7, SETLIM_2, FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SUPINF_1, ORDINAL1, FUNCT_7,
XXREAL_0, REAL_1, XXREAL_2, XCMPLX_0, XREAL_0, STRUCT_0, RELSET_1,
DOMAIN_1, FUNCT_1, PARTFUN1, FUNCT_2, NUMBERS, RCOMP_1, EQREL_1, BINOP_1,
REALSET1, PBOOLE, LATTICES, LATTICE3, NAT_LAT, REAL_LAT, MSUALG_3,
MSUALG_4, MSUALG_5, SETFAM_1, MSSUBFAM, CLOSURE2;
constructors BINOP_1, REAL_1, SQUARE_1, SUPINF_1, RCOMP_1, REALSET1, MSSUBFAM,
REAL_LAT, LATTICE3, MSUALG_3, MSUALG_5, CLOSURE2, XXREAL_2, RELSET_1,
FUNCT_7;
registrations XBOOLE_0, SUBSET_1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0,
MEMBERED, REALSET1, MSSUBFAM, STRUCT_0, LATTICES, LATTICE3, CLOSURE2,
ORDINAL1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
begin :: LATTICE OF MANY SORTED EQUIVALENCE RELATIONS IS COMPLETE
reserve I for non empty set;
reserve M for ManySortedSet of I;
reserve Y,x,y,i for set;
reserve r,r1,r2 for Real;
theorem :: MSUALG_7:1
id M is Equivalence_Relation of M;
theorem :: MSUALG_7:2
[|M,M|] is Equivalence_Relation of M;
registration
let I,M;
cluster EqRelLatt M -> bounded;
end;
theorem :: MSUALG_7:3
Bottom EqRelLatt M = id M;
theorem :: MSUALG_7:4
Top EqRelLatt M = [|M,M|];
theorem :: MSUALG_7:5
for X be Subset of EqRelLatt M holds X is SubsetFamily of [|M,M|];
theorem :: MSUALG_7:6
for a,b be Element of EqRelLatt M, A,B be Equivalence_Relation of
M st a = A & b = B holds a [= b iff A c= B;
theorem :: MSUALG_7:7
for X be Subset of EqRelLatt M, X1 be SubsetFamily of [|M,M|] st
X1 = X for a,b be Equivalence_Relation of M st a = meet |:X1:| & b in X holds a
c= b;
theorem :: MSUALG_7:8
for X be Subset of EqRelLatt M, X1 be SubsetFamily of [|M,M|] st
X1 = X & X is non empty holds meet |:X1:| is Equivalence_Relation of M;
definition
let L be non empty LattStr;
redefine attr L is complete means
:: MSUALG_7:def 1
for X being Subset of L ex a being
Element of L st X is_less_than a & for b being Element of L st X is_less_than b
holds a [= b;
end;
theorem :: MSUALG_7:9
EqRelLatt M is complete;
registration
let I,M;
cluster EqRelLatt M -> complete;
end;
theorem :: MSUALG_7:10
for X be Subset of EqRelLatt M, X1 be SubsetFamily of [|M,M|] st X1 =
X & X is non empty for a,b be Equivalence_Relation of M st a = meet |:X1:| & b
= "/\" (X,EqRelLatt M) holds a = b;
begin :: SUBLATTICES INHERITING SUP'S AND INF'S
definition
let L be Lattice;
let IT be SubLattice of L;
attr IT is /\-inheriting means
:: MSUALG_7:def 2
for X being Subset of IT holds "/\" (X ,L) in the carrier of IT;
attr IT is \/-inheriting means
:: MSUALG_7:def 3
for X being Subset of IT holds "\/" (X ,L) in the carrier of IT;
end;
theorem :: MSUALG_7:11
for L be Lattice, L9 be SubLattice of L, a,b be Element of L, a9
,b9 be Element of L9 st a = a9 & b = b9 holds a "\/" b = a9 "\/" b9 & a "/\" b
= a9 "/\" b9;
theorem :: MSUALG_7:12
for L be Lattice, L9 be SubLattice of L, X be Subset of L9, a be
Element of L, a9 be Element of L9 st a = a9 holds a is_less_than X iff a9
is_less_than X;
theorem :: MSUALG_7:13
for L be Lattice, L9 be SubLattice of L, X be Subset of L9, a be
Element of L, a9 be Element of L9 st a = a9 holds X is_less_than a iff X
is_less_than a9;
theorem :: MSUALG_7:14
for L be complete Lattice, L9 be SubLattice of L st L9 is
/\-inheriting holds L9 is complete;
theorem :: MSUALG_7:15
for L be complete Lattice, L9 be SubLattice of L st L9 is
\/-inheriting holds L9 is complete;
registration
let L be complete Lattice;
cluster complete for SubLattice of L;
end;
registration
let L be complete Lattice;
cluster /\-inheriting -> complete for SubLattice of L;
cluster \/-inheriting -> complete for SubLattice of L;
end;
theorem :: MSUALG_7:16
for L be complete Lattice, L9 be SubLattice of L st L9 is
/\-inheriting for A9 be Subset of L9 holds "/\" (A9,L) = "/\" (A9,L9);
theorem :: MSUALG_7:17
for L be complete Lattice, L9 be SubLattice of L st L9 is
\/-inheriting for A9 be Subset of L9 holds "\/" (A9,L) = "\/" (A9,L9);
theorem :: MSUALG_7:18
for L be complete Lattice, L9 be SubLattice of L st L9 is
/\-inheriting for A be Subset of L, A9 be Subset of L9 st A = A9 holds "/\" A =
"/\" A9;
theorem :: MSUALG_7:19
for L be complete Lattice, L9 be SubLattice of L st L9 is
\/-inheriting for A be Subset of L, A9 be Subset of L9 st A = A9 holds "\/" A =
"\/" A9;
begin :: SEGMENT OF REAL NUMBERS AS A COMPLETE LATTICE
definition
let r1,r2 such that
r1 <= r2;
func RealSubLatt(r1,r2) -> strict Lattice means
:: MSUALG_7:def 4
the carrier of it =
[.r1,r2.] & the L_join of it = maxreal||[.r1,r2.] & the L_meet of it = minreal
||[.r1,r2.];
end;
theorem :: MSUALG_7:20
for r1,r2 st r1 <= r2 holds RealSubLatt(r1,r2) is complete;
theorem :: MSUALG_7:21
ex L9 be SubLattice of RealSubLatt(In(0,REAL),In(1,REAL))
st L9 is \/-inheriting
non /\-inheriting;
theorem :: MSUALG_7:22
ex L be complete Lattice, L9 be SubLattice of L st L9 is \/-inheriting
non /\-inheriting;
theorem :: MSUALG_7:23
ex L9 be SubLattice of RealSubLatt(In(0,REAL),In(1,REAL))
st L9 is /\-inheriting
non \/-inheriting;
theorem :: MSUALG_7:24
ex L be complete Lattice, L9 be SubLattice of L st L9 is /\-inheriting
non \/-inheriting;