begin
:: deftheorem defines Inter INTERVA1:def 1 :
theorem Lemacik:
theorem KonceWInter:
theorem ThA2:
theorem
theorem NEmptyInter:
theorem Pik:
theorem Tha2:
theorem ThA1:
:: deftheorem WW defines IntervalSet INTERVA1:def 2 :
theorem
theorem ThB1:
theorem U2:
theorem LemmaA:
theorem LemmaB:
:: deftheorem defines _/\_ INTERVA1:def 3 :
:: deftheorem defines _\/_ INTERVA1:def 4 :
definition
let U be non
empty set ;
let A be non
empty IntervalSet of
U;
func A ``1 -> Subset of
U means :
Def4:
ex
B being
Subset of
U st
A = Inter it,
B;
existence
ex b1, B being Subset of U st A = Inter b1,B
uniqueness
for b1, b2 being Subset of U st ex B being Subset of U st A = Inter b1,B & ex B being Subset of U st A = Inter b2,B holds
b1 = b2
by Pik;
func A ``2 -> Subset of
U means :
Def5:
ex
B being
Subset of
U st
A = Inter B,
it;
existence
ex b1, B being Subset of U st A = Inter B,b1
uniqueness
for b1, b2 being Subset of U st ex B being Subset of U st A = Inter B,b1 & ex B being Subset of U st A = Inter B,b2 holds
b1 = b2
by Pik;
end;
:: deftheorem Def4 defines ``1 INTERVA1:def 5 :
:: deftheorem Def5 defines ``2 INTERVA1:def 6 :
theorem Wazne:
theorem Wazne33:
theorem wazne2:
theorem Un:
theorem Int:
:: deftheorem defines = INTERVA1:def 7 :
theorem
theorem
theorem
theorem
theorem Asso1:
theorem Prz1:
Lemacik1:
for X being set
for A, B, C being Subset-Family of X holds UNION A,(INTERSECTION B,C) c= INTERSECTION (UNION A,B),(UNION A,C)
:: deftheorem DefOr defines ordered INTERVA1:def 8 :
theorem nowosc1:
theorem CorNowosc1:
DefMi:
for X being set
for F being non empty ordered Subset-Family of X
for G being set st G in F holds
( G = min F iff for Y being set st Y in F holds
G c= Y )
DefMa:
for X being set
for F being non empty ordered Subset-Family of X
for G being set st G in F holds
( G = max F iff for Y being set st Y in F holds
Y c= G )
theorem nowosc2:
theorem Nowe1:
Nowe2:
for U being non empty set
for A being non empty IntervalSet of U holds A is non empty ordered Subset-Family of U
by CorNowosc1;
theorem Wazne1:
Lemacik2:
for X being set
for A, B, C being Subset-Family of X holds INTERSECTION A,(UNION B,C) c= UNION (INTERSECTION A,B),(INTERSECTION A,C)
theorem Wazne2:
theorem
theorem
theorem Wazne3:
theorem Wazne4:
theorem Abs1:
theorem Abs2:
begin
theorem Diff1:
theorem LemmaC0:
theorem LemmaC:
:: deftheorem defines _\_ INTERVA1:def 9 :
theorem Dif:
theorem Dif2:
theorem Dif3:
theorem Niep:
theorem Niep1:
:: deftheorem defines ^ INTERVA1:def 10 :
theorem ThDop0:
theorem ThDop1:
theorem
theorem
begin
theorem
theorem
theorem
theorem
theorem
theorem
begin
:: deftheorem DefAG defines IntervalSets INTERVA1:def 11 :
definition
let U be non
empty set ;
func InterLatt U -> non
empty strict LattStr means :
DefLLL:
( the
carrier of
it = IntervalSets U & ( for
a,
b being
Element of the
carrier of
it for
a9,
b9 being non
empty IntervalSet of
U st
a9 = a &
b9 = b holds
( the
L_join of
it . a,
b = a9 _\/_ b9 & the
L_meet of
it . a,
b = a9 _/\_ b9 ) ) );
existence
ex b1 being non empty strict LattStr st
( the carrier of b1 = IntervalSets U & ( for a, b being Element of the carrier of b1
for a9, b9 being non empty IntervalSet of U st a9 = a & b9 = b holds
( the L_join of b1 . a,b = a9 _\/_ b9 & the L_meet of b1 . a,b = a9 _/\_ b9 ) ) )
uniqueness
for b1, b2 being non empty strict LattStr st the carrier of b1 = IntervalSets U & ( for a, b being Element of the carrier of b1
for a9, b9 being non empty IntervalSet of U st a9 = a & b9 = b holds
( the L_join of b1 . a,b = a9 _\/_ b9 & the L_meet of b1 . a,b = a9 _/\_ b9 ) ) & the carrier of b2 = IntervalSets U & ( for a, b being Element of the carrier of b2
for a9, b9 being non empty IntervalSet of U st a9 = a & b9 = b holds
( the L_join of b2 . a,b = a9 _\/_ b9 & the L_meet of b2 . a,b = a9 _/\_ b9 ) ) holds
b1 = b2
end;
:: deftheorem DefLLL defines InterLatt INTERVA1:def 12 :
:: deftheorem Def19 defines RoughSet INTERVA1:def 13 :
theorem Def1:
:: deftheorem defines RS INTERVA1:def 14 :
:: deftheorem defines LAp INTERVA1:def 15 :
:: deftheorem defines UAp INTERVA1:def 16 :
:: deftheorem Def5 defines = INTERVA1:def 17 :
:: deftheorem defines _\/_ INTERVA1:def 18 :
:: deftheorem defines _/\_ INTERVA1:def 19 :
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem
theorem Th21:
theorem
theorem
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem
begin
:: deftheorem DefRSX defines RoughSets INTERVA1:def 20 :
:: deftheorem defines @ INTERVA1:def 21 :
:: deftheorem defines @ INTERVA1:def 22 :
definition
let X be
Tolerance_Space;
func RSLattice X -> strict LattStr means :
Def8:
( the
carrier of
it = RoughSets X & ( for
A,
B being
Element of
RoughSets X for
A9,
B9 being
RoughSet of
X st
A = A9 &
B = B9 holds
( the
L_join of
it . A,
B = A9 _\/_ B9 & the
L_meet of
it . A,
B = A9 _/\_ B9 ) ) );
existence
ex b1 being strict LattStr st
( the carrier of b1 = RoughSets X & ( for A, B being Element of RoughSets X
for A9, B9 being RoughSet of X st A = A9 & B = B9 holds
( the L_join of b1 . A,B = A9 _\/_ B9 & the L_meet of b1 . A,B = A9 _/\_ B9 ) ) )
uniqueness
for b1, b2 being strict LattStr st the carrier of b1 = RoughSets X & ( for A, B being Element of RoughSets X
for A9, B9 being RoughSet of X st A = A9 & B = B9 holds
( the L_join of b1 . A,B = A9 _\/_ B9 & the L_meet of b1 . A,B = A9 _/\_ B9 ) ) & the carrier of b2 = RoughSets X & ( for A, B being Element of RoughSets X
for A9, B9 being RoughSet of X st A = A9 & B = B9 holds
( the L_join of b2 . A,B = A9 _\/_ B9 & the L_meet of b2 . A,B = A9 _/\_ B9 ) ) holds
b1 = b2
end;
:: deftheorem Def8 defines RSLattice INTERVA1:def 23 :
Lm6:
for X being Tolerance_Space
for a, b being Element of (RSLattice X) holds a "\/" b = b "\/" a
Lm7:
for X being Tolerance_Space
for a, b, c being Element of (RSLattice X) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c
Lm8:
for X being Tolerance_Space
for K, L being Element of RoughSets X holds the L_join of (RSLattice X) . (the L_meet of (RSLattice X) . K,L),L = L
Lm9:
for X being Tolerance_Space
for a, b being Element of (RSLattice X) holds (a "/\" b) "\/" b = b
Lm10:
for X being Tolerance_Space
for a, b being Element of (RSLattice X) holds a "/\" b = b "/\" a
Lm11:
for X being Tolerance_Space
for a, b, c being Element of (RSLattice X) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c
Lm12:
for X being Tolerance_Space
for K, L, M being Element of RoughSets X holds the L_meet of (RSLattice X) . K,(the L_join of (RSLattice X) . L,M) = the L_join of (RSLattice X) . (the L_meet of (RSLattice X) . K,L),(the L_meet of (RSLattice X) . K,M)
Lm13:
for X being Tolerance_Space
for a, b being Element of (RSLattice X) holds a "/\" (a "\/" b) = a
:: deftheorem defines ERS INTERVA1:def 24 :
Th22:
for X being Tolerance_Space holds ERS X in RoughSets X
by DefRSX;
theorem Th23:
:: deftheorem defines TRS INTERVA1:def 25 :
Th24:
for X being Tolerance_Space holds TRS X in RoughSets X
by DefRSX;
theorem Th25:
theorem WazneX:
Th30:
for X being Tolerance_Space holds RSLattice X is complete