:: More on the Lattice of Many Sorted Equivalence Relations
:: by Robert Milewski
::
:: Received February 9, 1996
:: Copyright (c) 1996 Association of Mizar Users
theorem :: MSUALG_7:1
theorem Th2: :: MSUALG_7:2
theorem Th3: :: MSUALG_7:3
theorem :: MSUALG_7:4
theorem :: MSUALG_7:5
theorem Th6: :: MSUALG_7:6
theorem Th7: :: MSUALG_7:7
theorem Th8: :: MSUALG_7:8
theorem Th9: :: MSUALG_7:9
:: deftheorem Def1 defines complete MSUALG_7:def 1 :
theorem Th10: :: MSUALG_7:10
theorem :: MSUALG_7:11
:: deftheorem Def2 defines /\-inheriting MSUALG_7:def 2 :
:: deftheorem Def3 defines \/-inheriting MSUALG_7:def 3 :
theorem Th12: :: MSUALG_7:12
theorem Th13: :: MSUALG_7:13
theorem Th14: :: MSUALG_7:14
theorem Th15: :: MSUALG_7:15
theorem Th16: :: MSUALG_7:16
theorem Th17: :: MSUALG_7:17
theorem Th18: :: MSUALG_7:18
theorem :: MSUALG_7:19
theorem :: MSUALG_7:20
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.] )
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 :
theorem Th21: :: MSUALG_7:21
theorem Th22: :: MSUALG_7:22
theorem :: MSUALG_7:23
theorem Th24: :: MSUALG_7:24
theorem :: MSUALG_7:25