:: by Adam Naumowicz

::

:: Received April 3, 1998

:: Copyright (c) 1998-2019 Association of Mizar Users

:: Preliminaries

Lm1: 3 \ 2 c= 3 \ 1

proof end;

theorem Th5: :: YELLOW11:5

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 )

for a, b being Element of L holds

( a "/\" b = b iff a "\/" b = a )

proof end;

theorem Th6: :: YELLOW11:6

for L being LATTICE

for a, b, c being Element of L holds (a "/\" b) "\/" (a "/\" c) <= a "/\" (b "\/" c)

for a, b, c being Element of L holds (a "/\" b) "\/" (a "/\" c) <= a "/\" (b "\/" c)

proof end;

theorem Th7: :: YELLOW11:7

for L being LATTICE

for a, b, c being Element of L holds a "\/" (b "/\" c) <= (a "\/" b) "/\" (a "\/" c)

for a, b, c being Element of L holds a "\/" (b "/\" c) <= (a "\/" b) "/\" (a "\/" c)

proof end;

theorem Th8: :: YELLOW11:8

for L being LATTICE

for a, b, c being Element of L st a <= c holds

a "\/" (b "/\" c) <= (a "\/" b) "/\" c

for a, b, c being Element of L st a <= c holds

a "\/" (b "/\" c) <= (a "\/" b) "/\" c

proof end;

registration

correctness

coherence

( N_5 is strict & N_5 is reflexive & N_5 is transitive & N_5 is antisymmetric );

;

correctness

coherence

( N_5 is with_infima & N_5 is with_suprema );

end;
coherence

( N_5 is strict & N_5 is reflexive & N_5 is transitive & N_5 is antisymmetric );

;

correctness

coherence

( N_5 is with_infima & N_5 is with_suprema );

proof end;

registration

correctness

coherence

( M_3 is strict & M_3 is reflexive & M_3 is transitive & M_3 is antisymmetric );

;

correctness

coherence

( M_3 is with_infima & M_3 is with_suprema );

end;
coherence

( M_3 is strict & M_3 is reflexive & M_3 is transitive & M_3 is antisymmetric );

;

correctness

coherence

( M_3 is with_infima & M_3 is with_suprema );

proof end;

theorem Th9: :: YELLOW11:9

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,c,d,e are_mutually_distinct & 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 ) )

( 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,c,d,e are_mutually_distinct & 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

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,c,d,e are_mutually_distinct & 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 ) )

( 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,c,d,e are_mutually_distinct & 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;

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

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

for b_{1} being non empty reflexive antisymmetric with_infima RelStr st b_{1} is distributive holds

b_{1} is modular
end;

cluster non empty reflexive antisymmetric with_infima distributive -> non empty reflexive antisymmetric with_infima modular for RelStr ;

coherence for b

b

proof 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,c,d,e are_mutually_distinct 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

for L being LATTICE holds

( L is modular iff for K being full Sublattice of L holds not N_5 ,K are_isomorphic )

( 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,c,d,e are_mutually_distinct 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

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 )

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

ex b_{1} being Subset of L st

for c being Element of L holds

( c in b_{1} iff ( a <= c & c <= b ) )

for b_{1}, b_{2} being Subset of L st ( for c being Element of L holds

( c in b_{1} iff ( a <= c & c <= b ) ) ) & ( for c being Element of L holds

( c in b_{2} iff ( a <= c & c <= b ) ) ) holds

b_{1} = b_{2}

end;
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 for c being Element of L holds

( c in it iff ( a <= c & c <= b ) );

ex b

for c being Element of L holds

( c in b

proof end;

uniqueness for b

( c in b

( c in b

b

proof end;

:: deftheorem Def4 defines [# YELLOW11:def 4 :

for L being non empty RelStr

for a, b being Element of L

for b_{4} being Subset of L holds

( b_{4} = [#a,b#] iff for c being Element of L holds

( c in b_{4} iff ( a <= c & c <= b ) ) );

for L being non empty RelStr

for a, b being Element of L

for b

( b

( c in b

:: deftheorem 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#] );

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 ;

coherence

for b_{1} being Subset of L st not b_{1} is empty & b_{1} is interval holds

b_{1} is directed

for b_{1} being Subset of L st not b_{1} is empty & b_{1} is interval holds

b_{1} is filtered

end;
coherence

for b

b

proof end;

coherence for b

b

proof end;

registration
end;

theorem :: YELLOW11:13

for L being non empty reflexive transitive RelStr

for a, b being Element of L holds [#a,b#] = (uparrow a) /\ (downarrow b)

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;

coherence

subrelstr [#a,b#] is meet-inheriting

end;
let a, b be Element of L;

coherence

subrelstr [#a,b#] is meet-inheriting

proof end;

registration

let L be with_suprema Poset;

let a, b be Element of L;

coherence

subrelstr [#a,b#] is join-inheriting

end;
let a, b be Element of L;

coherence

subrelstr [#a,b#] is join-inheriting

proof end;

theorem :: YELLOW11:14

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

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

ex b_{1} being LATTICE st

( b_{1} is finite & not b_{1} is empty )
end;

cluster non empty finite V69() reflexive transitive antisymmetric with_suprema with_infima for RelStr ;

existence ex b

( b

proof end;

registration
end;

registration
end;