:: MSUALG_7 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem :: MSUALG_7:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, X being set holds
( x in the carrier of (EqRelLatt X) iff x is Equivalence_Relation of X )
proof end;

theorem Th2: :: MSUALG_7:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for M being ManySortedSet of I holds id M is Equivalence_Relation of M
proof end;

theorem Th3: :: MSUALG_7:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
EqRelLatt M is bounded
proof end;
end;

theorem :: MSUALG_7:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for M being ManySortedSet of I holds Bottom (EqRelLatt M) = id M
proof end;

theorem :: MSUALG_7:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for M being ManySortedSet of I holds Top (EqRelLatt M) = [|M,M|]
proof end;

theorem Th6: :: MSUALG_7:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th7: :: MSUALG_7:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th8: :: MSUALG_7:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th9: :: MSUALG_7:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :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 ) ) )
proof end;
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 Th10: :: MSUALG_7:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 -> bounded complete ;
coherence
EqRelLatt M is complete
by Th10;
end;

theorem :: MSUALG_7:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :Def2: :: MSUALG_7:def 2
for X being Subset of IT holds "/\" X,L in the carrier of IT;
attr IT 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 Th12: :: MSUALG_7:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for L' being SubLattice of L
for a, b being Element of L
for a', b' being Element of L' st a = a' & b = b' holds
( a "\/" b = a' "\/" b' & a "/\" b = a' "/\" b' )
proof end;

theorem Th13: :: MSUALG_7:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for L' being SubLattice of L
for X being Subset of L'
for a being Element of L
for a' being Element of L' st a = a' holds
( a is_less_than X iff a' is_less_than X )
proof end;

theorem Th14: :: MSUALG_7:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for L' being SubLattice of L
for X being Subset of L'
for a being Element of L
for a' being Element of L' st a = a' holds
( X is_less_than a iff X is_less_than a' )
proof end;

theorem Th15: :: MSUALG_7:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being complete Lattice
for L' being SubLattice of L st L' is /\-inheriting holds
L' is complete
proof end;

theorem Th16: :: MSUALG_7:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being complete Lattice
for L' being SubLattice of L st L' is \/-inheriting holds
L' is complete
proof end;

registration
let L be complete Lattice;
cluster complete SubLattice of L;
existence
ex b1 being SubLattice of L st b1 is complete
proof end;
end;

registration
let L be complete Lattice;
cluster /\-inheriting -> complete SubLattice of L;
coherence
for b1 being SubLattice of L st b1 is /\-inheriting holds
b1 is complete
by Th15;
cluster \/-inheriting -> complete SubLattice of L;
coherence
for b1 being SubLattice of L st b1 is \/-inheriting holds
b1 is complete
by Th16;
end;

theorem Th17: :: MSUALG_7:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being complete Lattice
for L' being SubLattice of L st L' is /\-inheriting holds
for A' being Subset of L' holds "/\" A',L = "/\" A',L'
proof end;

theorem Th18: :: MSUALG_7:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being complete Lattice
for L' being SubLattice of L st L' is \/-inheriting holds
for A' being Subset of L' holds "\/" A',L = "\/" A',L'
proof end;

theorem :: MSUALG_7:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being complete Lattice
for L' being SubLattice of L st L' is /\-inheriting holds
for A being Subset of L
for A' being Subset of L' st A = A' holds
"/\" A = "/\" A' by Th17;

theorem :: MSUALG_7:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being complete Lattice
for L' being SubLattice of L st L' is \/-inheriting holds
for A being Subset of L
for A' being Subset of L' st A = A' holds
"\/" A = "\/" A' by Th18;

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

theorem Th21: :: MSUALG_7:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r1, r2 being Real st r1 <= r2 holds
RealSubLatt r1,r2 is complete
proof end;

theorem Th22: :: MSUALG_7:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
ex L' being SubLattice of RealSubLatt 0,1 st
( L' is \/-inheriting & not L' is /\-inheriting )
proof end;

theorem :: MSUALG_7:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
ex L being complete Lattice ex L' being SubLattice of L st
( L' is \/-inheriting & not L' is /\-inheriting )
proof end;

theorem Th24: :: MSUALG_7:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
ex L' being SubLattice of RealSubLatt 0,1 st
( L' is /\-inheriting & not L' is \/-inheriting )
proof end;

theorem :: MSUALG_7:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
ex L being complete Lattice ex L' being SubLattice of L st
( L' is /\-inheriting & not L' is \/-inheriting )
proof end;