:: by Robert Milewski

::

:: Received February 9, 1996

:: Copyright (c) 1996-2021 Association of Mizar Users

registration
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|]

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 )

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

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

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 ;

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

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

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

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

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

registration
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

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;

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

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;

for X being Subset of IT holds "\/" (X,L) in the carrier of IT;

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

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

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 )

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 )

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 )

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

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

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

L9 is complete

proof end;

registration

let L be complete Lattice;

ex b_{1} being SubLattice of L st b_{1} is complete

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

existence ex b

proof end;

registration

let L be complete Lattice;

coherence

for b_{1} being SubLattice of L st b_{1} is /\-inheriting holds

b_{1} is complete
by Th14;

coherence

for b_{1} being SubLattice of L st b_{1} is \/-inheriting holds

b_{1} is complete
by Th15;

end;
coherence

for b

b

coherence

for b

b

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)

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)

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

theorem :: MSUALG_7:19

definition

let r1, r2 be Real;

assume A1: r1 <= r2 ;

ex b_{1} being strict Lattice st

( the carrier of b_{1} = [.r1,r2.] & the L_join of b_{1} = maxreal || [.r1,r2.] & the L_meet of b_{1} = minreal || [.r1,r2.] )

for b_{1}, b_{2} being strict Lattice st the carrier of b_{1} = [.r1,r2.] & the L_join of b_{1} = maxreal || [.r1,r2.] & the L_meet of b_{1} = minreal || [.r1,r2.] & the carrier of b_{2} = [.r1,r2.] & the L_join of b_{2} = maxreal || [.r1,r2.] & the L_meet of b_{2} = minreal || [.r1,r2.] holds

b_{1} = b_{2}
;

end;
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 ( the carrier of it = [.r1,r2.] & the L_join of it = maxreal || [.r1,r2.] & the L_meet of it = minreal || [.r1,r2.] );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def4 defines RealSubLatt MSUALG_7:def 4 :

for r1, r2 being Real st r1 <= r2 holds

for b_{3} being strict Lattice holds

( b_{3} = RealSubLatt (r1,r2) iff ( the carrier of b_{3} = [.r1,r2.] & the L_join of b_{3} = maxreal || [.r1,r2.] & the L_meet of b_{3} = minreal || [.r1,r2.] ) );

for r1, r2 being Real st r1 <= r2 holds

for b

( b

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 )

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

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

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

( L9 is /\-inheriting & not L9 is \/-inheriting )

proof end;