MSUALG_7: More on the Lattice of Many Sorted Equivalence Relations

:: More on the Lattice of Many Sorted Equivalence Relations
:: by Robert Milewski
::
:: Received February 9, 1996
:: Copyright (c) 1996-2016 Association of Mizar Users

environ

vocabularies HIDDEN, 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 HIDDEN, 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;
definitions TARSKI, LATTICE3, XXREAL_2;
theorems TARSKI, PBOOLE, MSSUBFAM, LATTICE3, VECTSP_8, MSUALG_4, MSUALG_5, ZFMISC_1, SETFAM_1, EQREL_1, LATTICES, NAT_LAT, FUNCT_1, REAL_LAT, FUNCT_2, RCOMP_1, MSUALG_3, CLOSURE2, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, NUMBERS, RELAT_1, XXREAL_2, XREAL_0;
schemes DOMAIN_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, REALSET1, MSSUBFAM, STRUCT_0, LATTICES, LATTICE3, CLOSURE2, ORDINAL1;
constructors HIDDEN, 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;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities BINOP_1, REALSET1;
expansions TARSKI, LATTICE3, XXREAL_2;

theorem Th1: :: MSUALG_7:1

for I being non empty set
for M being ManySortedSet of I holds id M is Equivalence_Relation of M

proof end;

theorem Th2: :: MSUALG_7:2

for I being non empty set
for M being ManySortedSet of I holds [|M,M|] is Equivalence_Relation of M

proof end;

registration

let I be non empty set ;
let M be ManySortedSet of I;

cluster EqRelLatt M -> bounded ;

coherence

proof end;

end;

theorem :: MSUALG_7:3

for I being non empty set
for M being ManySortedSet of I holds Bottom (EqRelLatt M) = id M

proof end;

theorem :: MSUALG_7:4

for I being non empty set
for M being ManySortedSet of I holds Top (EqRelLatt M) = [|M,M|]

proof end;

theorem Th5: :: MSUALG_7:5

for I being non empty set
for M being ManySortedSet of I
for X being Subset of (EqRelLatt M) holds X is SubsetFamily of [|M,M|]

proof end;

theorem Th6: :: MSUALG_7:6

for I being non empty set
for M being ManySortedSet of I
for a, b being Element of (EqRelLatt M)
for A, B being Equivalence_Relation of M st a = A & b = B holds
( a [= b iff A c= B )

proof end;

theorem Th7: :: MSUALG_7:7

for I being non empty set
for M being ManySortedSet of I
for X being Subset of (EqRelLatt M)
for X1 being SubsetFamily of [|M,M|] st X1 = X holds
for a, b being Equivalence_Relation of M st a = meet |:X1:| & b in X holds
a c= b

proof end;

theorem Th8: :: MSUALG_7:8

for I being non empty set
for M being ManySortedSet of I
for X being Subset of (EqRelLatt M)
for X1 being SubsetFamily of [|M,M|] st X1 = X & not X is empty holds
meet |:X1:| is Equivalence_Relation of M

proof end;

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

compatibility

proof end;

end;

:: deftheorem defines complete MSUALG_7:def 1 :

theorem Th9: :: MSUALG_7:9

for I being non empty set
for M being ManySortedSet of I holds EqRelLatt M is complete

proof end;

registration

let I be non empty set ;
let M be ManySortedSet of I;

cluster EqRelLatt M -> complete ;

coherence by Th9;

end;

theorem :: MSUALG_7:10

for I being non empty set
for M being ManySortedSet of I
for X being Subset of (EqRelLatt M)
for X1 being SubsetFamily of [|M,M|] st X1 = X & not X is empty holds
for a, b being Equivalence_Relation of M st a = meet |:X1:| & b = "/\" (X,(EqRelLatt M)) holds
a = b

proof end;

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;

:: deftheorem defines /\-inheriting MSUALG_7:def 2 :

:: deftheorem defines \/-inheriting MSUALG_7:def 3 :

theorem Th11: :: MSUALG_7:11

for L being Lattice
for L9 being SubLattice of L
for a, b being Element of L
for a9, b9 being Element of L9 st a = a9 & b = b9 holds
( a "\/" b = a9 "\/" b9 & a "/\" b = a9 "/\" b9 )

proof end;

theorem Th12: :: MSUALG_7:12

for L being Lattice
for L9 being SubLattice of L
for X being Subset of L9
for a being Element of L
for a9 being Element of L9 st a = a9 holds
( a is_less_than X iff a9 is_less_than X )

proof end;

theorem Th13: :: MSUALG_7:13

for L being Lattice
for L9 being SubLattice of L
for X being Subset of L9
for a being Element of L
for a9 being Element of L9 st a = a9 holds
( X is_less_than a iff X is_less_than a9 )

proof end;

theorem Th14: :: MSUALG_7:14

for L being complete Lattice
for L9 being SubLattice of L st L9 is /\-inheriting holds
L9 is complete

proof end;

theorem Th15: :: MSUALG_7:15

for L being complete Lattice
for L9 being SubLattice of L st L9 is \/-inheriting holds
L9 is complete

proof end;

registration

let L be complete Lattice;

cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete for SubLattice of L;

existence

proof end;

end;

registration

let L be complete Lattice;

cluster /\-inheriting -> complete for SubLattice of L;

coherence by Th14;

cluster \/-inheriting -> complete for SubLattice of L;

coherence by Th15;

end;

theorem Th16: :: MSUALG_7:16

for L being complete Lattice
for L9 being SubLattice of L st L9 is /\-inheriting holds
for A9 being Subset of L9 holds "/\" (A9,L) = "/\" (A9,L9)

proof end;

theorem Th17: :: MSUALG_7:17

for L being complete Lattice
for L9 being SubLattice of L st L9 is \/-inheriting holds
for A9 being Subset of L9 holds "\/" (A9,L) = "\/" (A9,L9)

proof end;

theorem :: MSUALG_7:18

for L being complete Lattice
for L9 being SubLattice of L st L9 is /\-inheriting holds
for A being Subset of L
for A9 being Subset of L9 st A = A9 holds
"/\" A = "/\" A9 by Th16;

theorem :: MSUALG_7:19

for L being complete Lattice
for L9 being SubLattice of L st L9 is \/-inheriting holds
for A being Subset of L
for A9 being Subset of L9 st A = A9 holds
"\/" A = "\/" A9 by Th17;

definition

let r1, r2 be Real;
assume A1: r1 <= r2 ;

func RealSubLatt (r1,r2) -> strict Lattice means :Def4: :: 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.] );

existence

proof end;

uniqueness ;

end;

:: deftheorem Def4 defines RealSubLatt MSUALG_7:def 4 :

theorem Th20: :: MSUALG_7:20

for r1, r2 being Real st r1 <= r2 holds
RealSubLatt (r1,r2) is complete

proof end;

reconsider jj = 1 as Real ;

reconsider jd = 1 / 2 as Real ;

theorem Th21: :: MSUALG_7:21

ex L9 being SubLattice of RealSubLatt ((In (0,REAL)),(In (1,REAL))) st
( L9 is \/-inheriting & not L9 is /\-inheriting )

proof end;

theorem :: MSUALG_7:22

ex L being complete Lattice ex L9 being SubLattice of L st
( L9 is \/-inheriting & not L9 is /\-inheriting )

proof end;

theorem Th23: :: MSUALG_7:23

ex L9 being SubLattice of RealSubLatt ((In (0,REAL)),(In (1,REAL))) st
( L9 is /\-inheriting & not L9 is \/-inheriting )

proof end;

theorem :: MSUALG_7:24

ex L being complete Lattice ex L9 being SubLattice of L st
( L9 is /\-inheriting & not L9 is \/-inheriting )

proof end;