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


begin

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

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

registration
let I be non empty set ;
let M be ManySortedSet of I;
cluster EqRelLatt M ->  bounded ;
coherence
 EqRelLatt M is bounded
proofend;
end;

theorem :: MSUALG_7:3
for I being non empty set
for M being ManySortedSet of I holds Bottom (EqRelLatt M) = id M
proofend;

theorem :: MSUALG_7:4
for I being non empty set
for M being ManySortedSet of I holds Top (EqRelLatt M) = [|M,M|]
proofend;

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|]
proofend;

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

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

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

definition
let L be non empty LattStr ;
redefine attr L is complete  means :Def1: :: 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
 ( L is complete iff 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 ) ) )
proofend;
end;

:: deftheorem Def1 defines complete MSUALG_7:def_1_:_
 for L being non empty LattStr holds
( L is complete iff 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 ) ) );

theorem Th9: :: MSUALG_7:9
for I being non empty set
for M being ManySortedSet of I holds EqRelLatt M is complete
proofend;

registration
let I be non empty set ;
let M be ManySortedSet of I;
cluster EqRelLatt M ->  complete ;
coherence
 EqRelLatt M is complete 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
proofend;

begin

definition
let L be Lattice;
let IT be SubLattice of L;
attrIT is /\-inheriting  means :Def2: :: MSUALG_7:def 2
 for X being Subset of IT holds "/\" (X,L) in the carrier of IT;
attrIT is \/-inheriting  means :Def3: :: MSUALG_7:def 3
 for X being Subset of IT holds "\/" (X,L) in the carrier of IT;
end;

:: deftheorem Def2 defines /\-inheriting MSUALG_7:def_2_:_
 for L being Lattice
for IT being SubLattice of L holds
( IT is /\-inheriting iff for X being Subset of IT holds "/\" (X,L) in the carrier of IT );

:: deftheorem Def3 defines \/-inheriting MSUALG_7:def_3_:_
 for L being Lattice
for IT being SubLattice of L holds
( IT is \/-inheriting iff for X being Subset of IT holds "\/" (X,L) in the carrier of IT );

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

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

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

theorem Th14: :: MSUALG_7:14
for L being complete Lattice
for L9 being SubLattice of L st L9 is /\-inheriting holds
L9 is complete
proofend;

theorem Th15: :: MSUALG_7:15
for L being complete Lattice
for L9 being SubLattice of L st L9 is \/-inheriting holds
L9 is complete
proofend;

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
 ex b1 being SubLattice of L st b1 is complete
proofend;
end;

registration
let L be complete Lattice;
cluster /\-inheriting  ->  complete for SubLattice of L;
coherence
 for b1 being SubLattice of L st b1 is /\-inheriting holds
b1 is complete by Th14;
cluster \/-inheriting  ->  complete for SubLattice of L;
coherence
 for b1 being SubLattice of L st b1 is \/-inheriting holds
b1 is complete 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)
proofend;

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

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;

begin

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.] &amp; the L_join of it = maxreal || [.r1,r2.] &amp; the L_meet of it = minreal || [.r1,r2.] );
existence
 ex b1 being strict Lattice st
( the carrier of b1 = [.r1,r2.] &amp; the L_join of b1 = maxreal || [.r1,r2.] &amp; the L_meet of b1 = minreal || [.r1,r2.] )
proofend;
uniqueness
 for b1, b2 being strict Lattice st the carrier of b1 = [.r1,r2.] &amp; the L_join of b1 = maxreal || [.r1,r2.] &amp; the L_meet of b1 = minreal || [.r1,r2.] &amp; the carrier of b2 = [.r1,r2.] &amp; the L_join of b2 = maxreal || [.r1,r2.] &amp; the L_meet of b2 = minreal || [.r1,r2.] holds
b1 = b2 ;
end;

:: deftheorem Def4 defines RealSubLatt MSUALG_7:def_4_:_
 for r1, r2 being Real st r1 <= r2 holds
for b3 being strict Lattice holds
( b3 = RealSubLatt (r1,r2) iff ( the carrier of b3 = [.r1,r2.] &amp; the L_join of b3 = maxreal || [.r1,r2.] &amp; the L_meet of b3 = minreal || [.r1,r2.] ) );

theorem Th20: :: MSUALG_7:20
for r1, r2 being Real st r1 <= r2 holds
RealSubLatt (r1,r2) is complete
proofend;

theorem Th21: :: MSUALG_7:21
ex L9 being SubLattice of RealSubLatt (0,1) st
( L9 is \/-inheriting &amp; not L9 is /\-inheriting )
proofend;

theorem :: MSUALG_7:22
ex L being complete Lattice ex L9 being SubLattice of L st
( L9 is \/-inheriting &amp; not L9 is /\-inheriting )
proofend;

theorem Th23: :: MSUALG_7:23
ex L9 being SubLattice of RealSubLatt (0,1) st
( L9 is /\-inheriting &amp; not L9 is \/-inheriting )
proofend;

theorem :: MSUALG_7:24
ex L being complete Lattice ex L9 being SubLattice of L st
( L9 is /\-inheriting &amp; not L9 is \/-inheriting )
proofend;