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

theorem Th1: :: YELLOW11:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
3 = {0,1,2}
proof end;

theorem Th2: :: YELLOW11:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
2 \ 1 = {1}
proof end;

theorem Th3: :: YELLOW11:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
3 \ 1 = {1,2}
proof end;

theorem Th4: :: YELLOW11:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
3 \ 2 = {2}
proof end;

Lm1: 3 \ 2 c= 3 \ 1
proof end;

theorem Th5: :: YELLOW11:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being reflexive antisymmetric with_suprema with_infima RelStr
for a, b being Element of L holds
( a "/\" b = b iff a "\/" b = a )
proof end;

theorem Th6: :: YELLOW11:6  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 a, b, c being Element of L holds (a "/\" b) "\/" (a "/\" c) <= a "/\" (b "\/" c)
proof end;

theorem Th7: :: YELLOW11:7  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 a, b, c being Element of L holds a "\/" (b "/\" c) <= (a "\/" b) "/\" (a "\/" c)
proof end;

theorem Th8: :: YELLOW11:8  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 a, b, c being Element of L st a <= c holds
a "\/" (b "/\" c) <= (a "\/" b) "/\" c
proof end;

definition
func N_5 -> RelStr equals :: YELLOW11:def 1
 InclPoset {0,(3 \ 1),2,(3 \ 2),3};
correctness
coherence
InclPoset {0,(3 \ 1),2,(3 \ 2),3} is RelStr ;
;
end;

:: deftheorem defines N_5 YELLOW11:def 1 :
N_5 = InclPoset {0,(3 \ 1),2,(3 \ 2),3};

registration
cluster N_5 -> strict reflexive transitive antisymmetric ;
correctness
coherence
( N_5 is strict & N_5 is reflexive & N_5 is transitive & N_5 is antisymmetric );
;
cluster N_5 -> with_suprema with_infima ;
correctness
coherence
( N_5 is with_infima & N_5 is with_suprema );
proof end;
end;

definition
func M_3 -> RelStr equals :: YELLOW11:def 2
 InclPoset {0,1,(2 \ 1),(3 \ 2),3};
correctness
coherence
InclPoset {0,1,(2 \ 1),(3 \ 2),3} is RelStr ;
;
end;

:: deftheorem defines M_3 YELLOW11:def 2 :
M_3 = InclPoset {0,1,(2 \ 1),(3 \ 2),3};

registration
cluster M_3 -> strict reflexive transitive antisymmetric ;
correctness
coherence
( M_3 is strict & M_3 is reflexive & M_3 is transitive & M_3 is antisymmetric );
;
cluster M_3 -> with_suprema with_infima ;
correctness
coherence
( M_3 is with_infima & M_3 is with_suprema );
proof end;
end;

theorem Th9: :: YELLOW11:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being LATTICE holds
( ex K being full Sublattice of L st N_5 ,K are_isomorphic iff ex a, b, c, d, e being Element of L st
( a <> b & a <> c & a <> d & a <> e & b <> c & b <> d & b <> e & c <> d & c <> e & d <> e & a "/\" b = a & a "/\" c = a & c "/\" e = c & d "/\" e = d & b "/\" c = a & b "/\" d = b & c "/\" d = a & b "\/" c = e & c "\/" d = e ) )
proof end;

theorem Th10: :: YELLOW11:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being LATTICE holds
( ex K being full Sublattice of L st M_3 ,K are_isomorphic iff ex a, b, c, d, e being Element of L st
( a <> b & a <> c & a <> d & a <> e & b <> c & b <> d & b <> e & c <> d & c <> e & d <> e & a "/\" b = a & a "/\" c = a & a "/\" d = a & b "/\" e = b & c "/\" e = c & d "/\" e = d & b "/\" c = a & b "/\" d = a & c "/\" d = a & b "\/" c = e & b "\/" d = e & c "\/" d = e ) )
proof end;

definition
let L be non empty RelStr ;
attr L is modular means :Def3: :: YELLOW11:def 3
for a, b, c being Element of L st a <= c holds
a "\/" (b "/\" c) = (a "\/" b) "/\" c;
end;

:: deftheorem Def3 defines modular YELLOW11:def 3 :
for L being non empty RelStr holds
( L is modular iff for a, b, c being Element of L st a <= c holds
a "\/" (b "/\" c) = (a "\/" b) "/\" c );

registration
cluster non empty reflexive antisymmetric with_infima distributive -> non empty reflexive antisymmetric with_infima modular RelStr ;
coherence
for b1 being non empty reflexive antisymmetric with_infima RelStr st b1 is distributive holds
b1 is modular
proof end;
end;

Lm2: for L being LATTICE holds
( L is modular iff for a, b, c, d, e being Element of L holds
( not a <> b or not a <> c or not a <> d or not a <> e or not b <> c or not b <> d or not b <> e or not c <> d or not c <> e or not d <> e or not a "/\" b = a or not a "/\" c = a or not c "/\" e = c or not d "/\" e = d or not b "/\" c = a or not b "/\" d = b or not c "/\" d = a or not b "\/" c = e or not c "\/" d = e ) )
proof end;

theorem :: YELLOW11:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being LATTICE holds
( L is modular iff for K being full Sublattice of L holds not N_5 ,K are_isomorphic )
proof end;

Lm3: for L being LATTICE st L is modular holds
( L is distributive iff for a, b, c, d, e being Element of L holds
( not a <> b or not a <> c or not a <> d or not a <> e or not b <> c or not b <> d or not b <> e or not c <> d or not c <> e or not d <> e or not a "/\" b = a or not a "/\" c = a or not a "/\" d = a or not b "/\" e = b or not c "/\" e = c or not d "/\" e = d or not b "/\" c = a or not b "/\" d = a or not c "/\" d = a or not b "\/" c = e or not b "\/" d = e or not c "\/" d = e ) )
proof end;

theorem :: YELLOW11: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 st L is modular holds
( L is distributive iff for K being full Sublattice of L holds not M_3 ,K are_isomorphic )
proof end;

definition
let L be non empty RelStr ;
let a, b be Element of L;
func [#a,b#] -> Subset of L means :Def4: :: YELLOW11:def 4
for c being Element of L holds
( c in it iff ( a <= c & c <= b ) );
existence
ex b1 being Subset of L st
for c being Element of L holds
( c in b1 iff ( a <= c & c <= b ) )
proof end;
uniqueness
for b1, b2 being Subset of L st ( for c being Element of L holds
( c in b1 iff ( a <= c & c <= b ) ) ) & ( for c being Element of L holds
( c in b2 iff ( a <= c & c <= b ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines [# YELLOW11:def 4 :
for L being non empty RelStr
for a, b being Element of L
for b4 being Subset of L holds
( b4 = [#a,b#] iff for c being Element of L holds
( c in b4 iff ( a <= c & c <= b ) ) );

definition
let L be non empty RelStr ;
let IT be Subset of L;
attr IT is interval means :Def5: :: YELLOW11:def 5
 ex a, b being Element of L st IT = [#a,b#];
end;

:: deftheorem Def5 defines interval YELLOW11:def 5 :
for L being non empty RelStr
for IT being Subset of L holds
( IT is interval iff ex a, b being Element of L st IT = [#a,b#] );

registration
let L be non empty reflexive transitive RelStr ;
cluster non empty interval -> directed Element of K10(the carrier of L);
coherence
for b1 being Subset of L st not b1 is empty & b1 is interval holds
b1 is directed
proof end;
cluster non empty interval -> filtered Element of K10(the carrier of L);
coherence
for b1 being Subset of L st not b1 is empty & b1 is interval holds
b1 is filtered
proof end;
end;

registration
let L be non empty RelStr ;
let a, b be Element of L;
cluster [#a,b#] -> interval ;
coherence
[#a,b#] is interval by Def5;
end;

theorem :: YELLOW11:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty reflexive transitive RelStr
for a, b being Element of L holds [#a,b#] = (uparrow a) /\ (downarrow b)
proof end;

registration
let L be with_infima Poset;
let a, b be Element of L;
cluster subrelstr [#a,b#] -> meet-inheriting ;
coherence
subrelstr [#a,b#] is meet-inheriting
proof end;
end;

registration
let L be with_suprema Poset;
let a, b be Element of L;
cluster subrelstr [#a,b#] -> join-inheriting ;
coherence
subrelstr [#a,b#] is join-inheriting
proof end;
end;

theorem :: YELLOW11: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 a, b being Element of L st L is modular holds
subrelstr [#b,(a "\/" b)#], subrelstr [#(a "/\" b),a#] are_isomorphic
proof end;

registration
cluster non empty finite RelStr ;
existence
ex b1 being LATTICE st
( b1 is finite & not b1 is empty )
proof end;
end;

registration
cluster finite -> lower-bounded RelStr ;
coherence
for b1 being Semilattice st b1 is finite holds
b1 is lower-bounded
proof end;
end;

registration
cluster finite -> complete RelStr ;
coherence
for b1 being LATTICE st b1 is finite holds
b1 is complete
proof end;
end;