:: Relational Formal Characterization of Rough Sets
:: by Adam Grabowski
::
:: Received January 17, 2013
:: Copyright (c) 2013 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies STRUCT_0, ORDERS_2, RELAT_1, TARSKI, ZFMISC_1, PRE_TOPC, RELAT_2,
XBOOLE_0, PARTFUN1, SUBSET_1, TOPS_1, FUNCT_1, FINSET_1, EQREL_1,
XXREAL_0, ROUGHS_1, RCOMP_1, ROUGHS_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1, RELAT_1, RELAT_2,
FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, DOMAIN_1, STRUCT_0, ORDERS_2,
EQREL_1, PRE_TOPC, TOPS_1, ROUGHS_1, YELLOW_3;
constructors EQREL_1, REALSET2, RELSET_1, ROUGHS_1, YELLOW_3, TOPS_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FINSET_1, NAT_1, STRUCT_0,
ORDERS_2, RELSET_1, FUNCT_1, FUNCT_2, YELLOW_3, TOPS_1, PRE_TOPC;
requirements BOOLE, SUBSET, NUMERALS;
definitions TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, RELAT_1, FUNCT_2, ROUGHS_1;
equalities TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, RELAT_1, FUNCT_2, ROUGHS_1;
expansions TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, RELAT_1, FUNCT_2, ROUGHS_1;
theorems EQREL_1, XBOOLE_0, XBOOLE_1, SUBSET_1, TARSKI, ZFMISC_1, RELAT_1,
RELAT_2, FUNCT_2, FUNCT_1, ORDERS_2, YELLOW_3, RELSET_1, PARTFUN1,
XTUPLE_0, TDLAT_3, PRE_TOPC, TOPS_1;
schemes FUNCT_2, RELSET_1, CHAIN_1;
begin :: Preliminaries
registration
cluster non empty void for RelStr;
existence
proof
reconsider E = {} as Relation of 1 by RELSET_1:12;
set X = RelStr (# 1, E #);
reconsider X as non empty RelStr;
X is void;
hence thesis;
end;
end;
theorem help0:
for R being total non empty RelStr,
x being Element of R holds
x in field the InternalRel of R
proof
let R be total non empty RelStr;
let x be Element of R;
dom the InternalRel of R = the carrier of R by PARTFUN1:def 2;
hence thesis by XBOOLE_0:def 3;
end;
theorem Th2:
for R being non empty 1-sorted,
X being Subset of R holds
{ x where x is Element of R : {} c= X } = [#]R
proof
let R be non empty 1-sorted;
let X be Subset of R;
thus { x where x is Element of R : {} c= X } c= [#]R
proof
let y be element;
assume y in { x where x is Element of R : {} c= X }; then
ex z being Element of R st z = y & {} c= X;
hence thesis;
end;
let y be element;
assume
B2: y in [#]R;
y in { x where x is Element of R : {} c= X}
proof
assume not y in { x where x is Element of R : {} c= X }; then
not y is Element of R or not {} c= X;
hence contradiction by B2;
end;
hence thesis;
end;
theorem Th3:
for R being 1-sorted,
X being Subset of R holds
{ x where x is Element of R : {} meets X } = {}R
proof
let R be 1-sorted;
let X be Subset of R;
thus {x where x is Element of R : {} meets X} c= {}R
proof
let y be element;
assume y in {x where x is Element of R : {} meets X}; then
ex z being Element of R st z = y & {} meets X;
then {} /\ X <> {} by XBOOLE_0:def 7;
hence thesis;
end;
thus thesis;
end;
begin :: Missing Ordinary Properties of Binary Relations
definition let R be Relation, X be set;
pred R is_serial_in X means :Def0:
for x being element st x in X holds
ex y being element st y in X & [x,y] in R;
end;
definition let R be Relation;
attr R is serial means
R is_serial_in field R;
end;
definition let R be RelStr;
attr R is serial means :Def2:
the InternalRel of R is_serial_in the carrier of R;
end;
Kuku:
for R being RelStr st
the InternalRel of R is_reflexive_in the carrier of R holds
R is serial
proof
let R be RelStr;
assume
A1: the InternalRel of R is_reflexive_in the carrier of R;
set IR = the InternalRel of R, X = the carrier of R;
for x being element st x in X
ex y being element st y in X & [x,y] in IR
proof
let x be element;
assume
A2: x in X; then
[x,x] in IR by A1,RELAT_2:def 1;
hence thesis by A2;
end;
hence thesis by Def0;
end;
registration
cluster reflexive -> serial for RelStr;
coherence
proof
let R be RelStr;
assume R is reflexive;
hence thesis by Kuku,ORDERS_2:def 2;
end;
end;
definition let R be non empty RelStr;
redefine attr R is serial means
for x being Element of R ex y being Element of R st x <= y;
compatibility
proof
thus R is serial implies
for x being Element of R ex y being Element of R st x <= y
proof
assume
b: R is serial;
set IR = the InternalRel of R, X = the carrier of R;
let x be Element of R;
consider y being element such that
B1: y in X & [x,y] in IR by Def0,b;
thus thesis by B1,ORDERS_2:def 5;
end;
assume
G1: for x being Element of R ex y being Element of R st x <= y;
the InternalRel of R is_serial_in the carrier of R
proof
let x be element;
assume x in the carrier of R; then
reconsider xx = x as Element of R;
consider y being Element of R such that
Z1: xx <= y by G1;
take y;
thus thesis by Z1,ORDERS_2:def 5;
end;
hence thesis;
end;
end;
registration
cluster total -> serial for RelStr;
coherence
proof
let R be RelStr;
set RR = the InternalRel of R, X = the carrier of R;
assume R is total; then
s1: dom RR = X by PARTFUN1:def 2;
RR is_serial_in X
proof
let x be element;
assume x in X; then
consider y being element such that
Z1: [x,y] in RR by s1,RELSET_1:9;
take y;
consider xx,yy being element such that
Z2: [x,y] = [xx,yy] & xx in X & yy in X by Z1,RELSET_1:2;
thus thesis by Z1,Z2,XTUPLE_0:1;
end;
hence thesis;
end;
cluster serial -> total for RelStr;
coherence
proof
let R be RelStr;
set RR = the InternalRel of R, X = the carrier of R;
assume
s: R is serial;
for x being element st x in X
ex y being element st [x,y] in RR
proof
let x be element;
assume x in X; then
ex y being element st y in X & [x,y] in RR by Def0,s;
hence thesis;
end; then
dom RR = X by RELSET_1:9; then
RR is total by PARTFUN1:def 2;
hence thesis by ORDERS_2:def 1;
end;
end;
help2:
for R being non empty serial RelStr,
x being Element of R holds
Class (the InternalRel of R,x) <> {}
proof
let R be non empty serial RelStr;
let x be Element of R;
A1: x in {x} by TARSKI:def 1;
consider y being element such that
A2: y in the carrier of R & [x,y] in the InternalRel of R by Def0,Def2;
thus thesis by RELAT_1:def 13,A2,A1;
end;
registration let R be non empty serial RelStr,
x be Element of R;
cluster Class (the InternalRel of R,x) -> non empty;
coherence by help2;
end;
:: Reflexive relations
theorem help3:
for R being non empty reflexive RelStr,
x being Element of R holds
x in Class (the InternalRel of R,x)
proof
let R be non empty reflexive RelStr;
let x be Element of R;
A1: x in field the InternalRel of R by help0;
A2: x in {x} by TARSKI:def 1;
[x,x] in the InternalRel of R by A1,RELAT_2:def 1,RELAT_2:def 9;
hence thesis by RELAT_1:def 13,A2;
end;
registration let R be non empty reflexive RelStr,
x be Element of R;
cluster Class (the InternalRel of R,x) -> non empty;
coherence;
end;
:: Mediate relations
definition let R be Relation, X be set;
pred R is_mediate_in X means :DefM1:
for x,y being element st x in X & y in X holds
[x,y] in R implies
ex z being element st z in X & [x,z] in R & [z,y] in R;
end;
definition let R be Relation;
attr R is mediate means
R is_mediate_in field R;
end;
definition let R be RelStr;
attr R is mediate means :DefM2:
the InternalRel of R is_mediate_in the carrier of R;
end;
registration
cluster reflexive -> mediate for RelStr;
coherence
proof
let R be RelStr;
assume A1: R is reflexive;
set IR = the InternalRel of R, X = the carrier of R;
for x,y being element
st x in X & y in X holds [x,y] in the InternalRel of R implies
ex z being element st z in X & [x,z] in IR & [z,y] in IR
proof
let x,y be element;
assume B1: x in X & y in X;
assume B2: [x,y] in IR;
[x,x] in IR by B1,RELAT_2:def 1,A1,ORDERS_2:def 2;
hence thesis by B1,B2;
end;
hence thesis by DefM1;
end;
end;
begin :: Approximations Revisited
theorem help7:
for R being non empty RelStr,
a, b being Element of R st
a in UAp ({b}) holds [a,b] in the InternalRel of R
proof
let R be non empty RelStr;
let a, b be Element of R;
assume a in UAp ({b}); then
consider x being Element of R such that
A1: x = a & Class (the InternalRel of R,x) meets {b};
consider y being element such that
A2: y in Class (the InternalRel of R,x) /\ {b} by A1,XBOOLE_0:def 1;
y in Class (the InternalRel of R,x) & y in {b} by XBOOLE_0:def 4,A2; then
y = b & y in Class (the InternalRel of R,x) by TARSKI:def 1;
hence thesis by A1,RELAT_1:169;
end;
definition let R be non empty RelStr;
let X be Subset of R;
func Uap X -> Subset of R equals
(LAp X`)`;
coherence;
end;
definition let R be non empty RelStr;
let X be Subset of R;
func Lap X -> Subset of R equals
(UAp X`)`;
coherence;
end;
theorem Th8R:
for R being non empty RelStr,
X being Subset of R
for x being element st x in LAp X holds
Class (the InternalRel of R, x) c= X
proof
let R be non empty RelStr,
X be Subset of R;
let x be element;
assume x in LAp X; then
ex x1 being Element of R st x = x1 &
Class (the InternalRel of R, x1) c= X;
hence thesis;
end;
theorem Th10R:
for R being non empty RelStr,
X being Subset of R
for x being set st x in UAp X holds
Class (the InternalRel of R, x) meets X
proof
let R be non empty RelStr,
X be Subset of R;
let x be set;
assume x in UAp X;
then ex x1 being Element of R st
x = x1 & Class (the InternalRel of R, x1) meets X;
hence thesis;
end;
theorem Mu1:
for R being non empty RelStr,
X being Subset of R holds
Uap X = UAp X
proof
let R be non empty RelStr,
X be Subset of R;
AA: LAp X` misses UAp X
proof
assume LAp X` meets UAp X;
then consider x being element such that
A1: x in LAp X` & x in UAp X by XBOOLE_0:3;
Class (the InternalRel of R, x) meets X &
Class (the InternalRel of R, x) c= X` by A1,Th8R,Th10R;
hence thesis by XBOOLE_1:63,79;
end;
(UAp X)` c= LAp X`
proof let x be element;
assume
A2: x in (UAp X)`;
then not x in UAp X by XBOOLE_0:def 5;
then Class (the InternalRel of R, x) misses X by A2;
then Class (the InternalRel of R, x) c= X` by SUBSET_1:23;
hence x in LAp X` by A2;
end;
hence thesis by AA,SUBSET_1:17,23;
end;
theorem Mu2:
for R being non empty RelStr,
X being Subset of R holds
Lap X = LAp X
proof
let R be non empty RelStr,
X be Subset of R;
Uap X` = UAp X` by Mu1;
hence thesis;
end;
theorem :: Example 2
for R being non empty void RelStr,
X being Subset of R holds
LAp X = [#]R
proof
let R be non empty void RelStr,
X be Subset of R;
B1: the InternalRel of R = {} by YELLOW_3:def 3;
{ x where x is Element of R : Class ({}, x) c= X } =
{ x where x is Element of R : {} c= X }
proof
thus { x where x is Element of R : Class ({}, x) c= X } c=
{ x where x is Element of R : {} c= X }
proof
let y be element;
assume y in { x where x is Element of R : Class ({}, x) c= X }; then
consider z being Element of R such that
C1: z = y & Class ({}, z) c= X;
thus thesis by C1;
end;
let y be element;
assume y in { x where x is Element of R : {} c= X }; then
consider z being Element of R such that
C1: z = y & {} c= X;
Class ({},z) c= X;
hence thesis by C1;
end;
hence thesis by Th2,B1;
end;
theorem :: Example 2
for R being non empty void RelStr,
X being Subset of R holds
UAp X = {}R
proof
let R be non empty void RelStr,
X be Subset of R;
B1: the InternalRel of R = {} by YELLOW_3:def 3;
{ x where x is Element of R : Class ({},x) meets X } =
{ x where x is Element of R : {} meets X}
proof
thus { x where x is Element of R : Class ({},x) meets X } c=
{ x where x is Element of R : {} meets X}
proof
let y be element;
assume y in { x where x is Element of R : Class ({},x) meets X }; then
consider z being Element of R such that
a1: z = y & Class ({},z) meets X;
thus thesis by a1;
end;
let y be element;
assume y in { x where x is Element of R : {} meets X}; then
consider z being Element of R such that
a1: z = y & {} meets X;
thus thesis by a1;
end;
hence thesis by Th3,B1;
end;
begin :: General Properties of Approximations
registration
let R be non empty RelStr;
reduce LAp ([#]R) to [#]R;
reducibility
proof
{x where x is Element of R : Class (the InternalRel of R,x) c= [#]R} = [#]R
proof
thus { x where x is Element of R :
Class (the InternalRel of R,x) c= [#]R } c= [#]R
proof
let y be element;
assume y in { x where x is Element of R :
Class (the InternalRel of R,x) c= [#]R}; then
ex z being Element of R st z = y &
Class (the InternalRel of R,z) c= [#]R;
hence thesis;
end;
let y be element;
assume
A1: y in [#]R;
assume not y in { x where x is Element of R :
Class (the InternalRel of R,x) c= [#]R}; then
not y is Element of R or not Class (the InternalRel of R,y) c= [#]R;
hence contradiction by A1;
end;
hence thesis;
end;
end;
registration
let R be non empty serial RelStr;
reduce UAp ([#]R) to [#]R;
reducibility
proof
[#]R c= UAp ([#]R)
proof
let y be element;
assume
A1: y in [#]R; then
Class (the InternalRel of R, y) meets [#]R by XBOOLE_1:28;
hence thesis by A1;
end;
hence thesis;
end;
end;
registration
let R be non empty serial RelStr;
reduce LAp {}R to {}R;
reducibility
proof
{x where x is Element of R :
Class (the InternalRel of R, x) c= {}R} c= {}R
proof
let y be element;
assume y in { x where x is Element of R :
Class (the InternalRel of R, x) c= {}R}; then
consider z being Element of R such that
A2: z = y & Class (the InternalRel of R,z) c= {}R;
thus thesis by A2;
end;
hence thesis;
end;
end;
registration
let R be non empty RelStr;
reduce UAp ({}R) to {}R;
reducibility
proof
thus UAp {}R c= {}R
proof
let y be element;
assume y in UAp {}R; then
consider z being Element of R such that
B2: y = z & Class (the InternalRel of R, z) meets {}R;
thus thesis by B2;
end;
thus thesis;
end;
end;
theorem :: Proposition 2 4L
for R being non empty RelStr,
X, Y being Subset of R holds
LAp (X /\ Y) = LAp (X) /\ LAp (Y)
proof
let R be non empty RelStr;
let X, Y be Subset of R;
{ x where x is Element of R : Class (the InternalRel of R,x) c= X /\ Y} =
{ x where x is Element of R : Class (the InternalRel of R,x) c= X } /\
{ x where x is Element of R : Class (the InternalRel of R,x) c= Y}
proof
thus
{x where x is Element of R : Class (the InternalRel of R,x) c= X /\ Y} c=
{ x where x is Element of R : Class (the InternalRel of R,x) c= X } /\
{ x where x is Element of R : Class (the InternalRel of R,x) c= Y}
proof
let y be element;
assume y in { x where x is Element of R :
Class (the InternalRel of R,x) c= X /\ Y}; then
consider z being Element of R such that
B2: z = y & Class (the InternalRel of R,z) c= X /\ Y;
X /\ Y c= X & X /\ Y c= Y by XBOOLE_1:17; then
Class (the InternalRel of R,z) c= X &
Class (the InternalRel of R,z) c= Y by B2; then
z in {x where x is Element of R : Class (the InternalRel of R,x) c= X}&
z in {x where x is Element of R : Class (the InternalRel of R,x) c= Y};
hence thesis by B2,XBOOLE_0:def 4;
end;
let y be element;
assume B1: y in { x where x is Element of R :
Class (the InternalRel of R,x) c= X } /\
{x where x is Element of R : Class (the InternalRel of R,x) c= Y}; then
B2: y in { x where x is Element of R :
Class (the InternalRel of R,x) c= X } by XBOOLE_0:def 4;
B4: y in { x where x is Element of R :
Class (the InternalRel of R,x) c= Y} by XBOOLE_0:def 4,B1;
consider z being Element of R such that
B3: z = y & Class (the InternalRel of R,z) c= X by B2;
consider w being Element of R such that
B5: w = y & Class (the InternalRel of R,w) c= Y by B4;
Class (the InternalRel of R,z) /\
Class (the InternalRel of R,z) c= X /\ Y by B3,XBOOLE_1:27,B5;
hence thesis by B3;
end;
hence thesis;
end;
theorem P24H: :: Proposition 2 4H
for R being non empty RelStr,
X, Y being Subset of R holds
UAp (X \/ Y) = UAp X \/ UAp Y
proof
let R be non empty RelStr;
let X, Y be Subset of R;
thus UAp (X \/ Y) c= UAp X \/ UAp Y
proof
let y be element;
assume y in UAp (X \/ Y); then
consider z being Element of R such that
A1: z = y & Class (the InternalRel of R, z) meets (X \/ Y);
Class (the InternalRel of R, z) meets X or
Class (the InternalRel of R, z) meets Y by A1,XBOOLE_1:70; then
z in { x where x is Element of R :
Class (the InternalRel of R, x) meets X} or
z in { x where x is Element of R :
Class (the InternalRel of R, x) meets Y};
hence thesis by A1,XBOOLE_0:def 3;
end;
let y be element;
assume y in UAp X \/ UAp Y; then
per cases by XBOOLE_0:def 3;
suppose y in UAp X; then
consider z being Element of R such that
C1: z = y & Class (the InternalRel of R, z) meets X;
Class (the InternalRel of R, z) meets (X \/ Y) by C1,XBOOLE_1:70;
hence thesis by C1;
end;
suppose y in UAp Y; then
consider z being Element of R such that
C1: z = y & Class (the InternalRel of R, z) meets Y;
Class (the InternalRel of R, z) meets (X \/ Y) by C1,XBOOLE_1:70;
hence thesis by C1;
end;
end;
theorem :: Proposition 2 6L
for R being non empty RelStr,
X, Y being Subset of R st
X c= Y holds LAp X c= LAp Y
proof
let R be non empty RelStr;
let X, Y be Subset of R;
assume
A0: X c= Y;
let y be element;
assume y in LAp X; then
consider z being Element of R such that
A2: z = y & Class (the InternalRel of R, z) c= X;
Class (the InternalRel of R, z) c= Y by A0,A2;
hence thesis by A2;
end;
theorem ThUzaw: :: Proposition 2 6H
for R being non empty RelStr,
X, Y being Subset of R st
X c= Y holds UAp X c= UAp Y
proof
let R be non empty RelStr;
let X, Y be Subset of R;
assume
A0: X c= Y;
let y be element;
assume y in UAp X; then
consider z being Element of R such that
A2: z = y & Class (the InternalRel of R, z) meets X;
Class (the InternalRel of R, z) meets Y by A0,A2,XBOOLE_1:63;
hence thesis by A2;
end;
theorem Th8LH: :: Proposition 2 8LH
for R being non empty RelStr,
X being Subset of R holds
LAp (X`) = (UAp X)`
proof
let R be non empty RelStr;
let X be Subset of R;
thus LAp (X`) c= (UAp X)`
proof
let y be element;
assume y in LAp (X`); then
consider z being Element of R such that
B2: z = y & Class (the InternalRel of R, z) c= X`;
not z in { x where x is Element of R :
Class (the InternalRel of R, x) meets X }
proof
assume z in { x where x is Element of R :
Class (the InternalRel of R, x) meets X }; then
consider t being Element of R such that
B4: t = z & Class (the InternalRel of R, t) meets X;
thus contradiction by B2,SUBSET_1:23,B4;
end;
hence thesis by B2,XBOOLE_0:def 5;
end;
let y be element;
assume
B0: y in (UAp X)`;
y in [#]R & not y in UAp X by XBOOLE_0:def 5,B0; then
not (Class (the InternalRel of R, y) meets X); then
Class (the InternalRel of R, y) c= X` by SUBSET_1:23;
hence thesis by B0;
end;
theorem Th9LH: :: Proposition 2 9LH
for R being non empty serial RelStr,
X being Subset of R holds
LAp X c= UAp X
proof
let R be non empty serial RelStr;
let X be Subset of R;
let y be element;
assume y in LAp X; then
consider z being Element of R such that
A1: z = y & Class (the InternalRel of R, z) c= X;
Class (the InternalRel of R, z) meets X by XBOOLE_1:69,A1;
hence thesis by A1;
end;
begin :: Auxiliary Operation on Approximation Operators
definition let R be non empty RelStr;
func LAp R -> Function of bool the carrier of R, bool the carrier of R
means :DefL:
for X being Subset of R holds it.X = LAp X;
existence
proof
deffunc F(Element of bool the carrier of R) = LAp $1;
ex f being Function of bool the carrier of R, bool the carrier of R st
for X being Element of bool the carrier of R holds f.X = F(X)
from FUNCT_2:sch 4; then
consider f being Function of bool the carrier of R, bool the carrier of R
such that
B1: for X being Subset of R holds f.X = F(X);
take f;
let r be Subset of R;
thus thesis by B1;
end;
uniqueness
proof
let f,g be Function of bool the carrier of R, bool the carrier of R
such that
A1: for X being Subset of R holds f.X = LAp X and
A2: for X being Subset of R holds g.X = LAp X;
let Y be Subset of R;
thus f.Y = LAp Y by A1
.= g.Y by A2;
end;
func UAp R -> Function of bool the carrier of R, bool the carrier of R
means :DefU:
for X being Subset of R holds it.X = UAp X;
existence
proof
deffunc F(Element of bool the carrier of R) = UAp $1;
ex f being Function of bool the carrier of R, bool the carrier of R st
for X being Element of bool the carrier of R holds f.X = F(X)
from FUNCT_2:sch 4; then
consider f being Function of bool the carrier of R, bool the carrier of R
such that
B1: for X being Subset of R holds f.X = F(X);
take f;
let r be Subset of R;
thus thesis by B1;
end;
uniqueness
proof
let f,g be Function of bool the carrier of R, bool the carrier of R
such that
A1: for X being Subset of R holds f.X = UAp X and
A2: for X being Subset of R holds g.X = UAp X;
let Y be Subset of R;
thus f.Y = UAp Y by A1
.= g.Y by A2;
end;
end;
definition
let A be non empty set;
let U be Function of bool A, bool A;
attr U is empty-preserving means :EP:
U.{} = {};
attr U is universe-preserving means :UP:
U.A = A;
end;
registration let A be non empty set;
cluster id bool A -> empty-preserving universe-preserving
for Function of bool A, bool A;
coherence
proof
reconsider f = id bool A as Function of bool A, bool A;
{} c= A; then
a1: f.{} = {} by FUNCT_1:18;
A in bool A by ZFMISC_1:def 1; then
f.A = A by FUNCT_1:18;
hence thesis by a1,UP,EP;
end;
end;
registration let A be non empty set;
cluster empty-preserving universe-preserving for
Function of bool A, bool A;
existence
proof
reconsider f = id bool A as Function of bool A, bool A;
f is empty-preserving universe-preserving;
hence thesis;
end;
end;
definition let X be set;
let f be Function of bool X, bool X;
func Flip f -> Function of bool X, bool X means :FlipDef:
for x being Subset of X holds
it.x = (f.x`)`;
existence
proof
deffunc F(Element of bool X) = (f.$1`)`;
ex g being Function of bool X, bool X st
for x being Element of bool X holds g.x = F(x) from FUNCT_2:sch 4; then
consider g being Function of bool X, bool X such that
A1: for x being Element of bool X holds g.x = F(x);
take g;
let x be Subset of X;
thus thesis by A1;
end;
uniqueness
proof
let f1, f2 be Function of bool X, bool X such that
A1: for x being Subset of X holds f1.x = (f.x`)` and
A2: for x being Subset of X holds f2.x = (f.x`)`;
let x be Subset of X;
thus f1.x = (f.x`)` by A1 .= f2.x by A2;
end;
end;
theorem Lm1:
for X being set,
f being Function of bool X, bool X st
f.{} = {} holds
(Flip f).X = X
proof
let X be set,
f be Function of bool X, bool X;
assume
A1: f.{} = {};
X c= X; then
reconsider y = X as Subset of X;
(Flip f).y = (f.y`)` by FlipDef
.= ({}X)` by A1
.= y;
hence thesis;
end;
theorem EmFix:
for X being set,
f being Function of bool X, bool X st
f.X = X holds
(Flip f).{} = {}
proof
let X be set,
f be Function of bool X, bool X;
assume
A1: f.X = X;
set y = {}X;
(Flip f).y = (f.y`)` by FlipDef
.= {}X by A1;
hence thesis;
end;
theorem
for X being set,
f being Function of bool X, bool X st
f = id bool X holds
Flip f = f
proof
let X be set,
f be Function of bool X, bool X;
assume
A1: f = id bool X;
for x being Subset of X holds (Flip f).x = f.x
proof
let x be Subset of X;
thus (Flip f).x = (f.x`)` by FlipDef
.= x`` by A1,FUNCT_1:18
.= f.x by A1,FUNCT_1:18;
end;
hence thesis;
end;
theorem
for X being set,
f being Function of bool X, bool X st
for A, B being Subset of X holds f.(A \/ B) = f.A \/ f.B holds
for A, B being Subset of X holds
(Flip f).(A /\ B) = (Flip f).A /\ (Flip f).B
proof
let X be set,
f be Function of bool X, bool X;
assume
A1: for A, B being Subset of X holds f.(A \/ B) = f.A \/ f.B;
let A, B be Subset of X;
set g = Flip f;
g.(A /\ B) = (f.(A /\ B)`)` by FlipDef
.= (f.(A` \/ B`))` by XBOOLE_1:54
.= (f.(A`) \/ f.(B`))` by A1
.= (f.(A`))` /\ (f.(B`))` by XBOOLE_1:53
.= g.A /\ (f.(B`))` by FlipDef
.= g.A /\ g.B by FlipDef;
hence thesis;
end;
theorem FlSum:
for X being set,
f being Function of bool X, bool X st
for A, B being Subset of X holds f.(A /\ B) = f.A /\ f.B holds
for A, B being Subset of X holds
(Flip f).(A \/ B) = (Flip f).A \/ (Flip f).B
proof
let X be set,
f be Function of bool X, bool X;
assume
A1: for A, B being Subset of X holds f.(A /\ B) = f.A /\ f.B;
let A, B be Subset of X;
set g = Flip f;
g.(A \/ B) = (f.(A \/ B)`)` by FlipDef
.= (f.(A` /\ B`))` by XBOOLE_1:53
.= (f.(A`) /\ f.(B`))` by A1
.= (f.(A`))` \/ (f.(B`))` by XBOOLE_1:54
.= g.A \/ (f.(B`))` by FlipDef
.= g.A \/ g.B by FlipDef;
hence thesis;
end;
theorem FlInv:
for X being set,
f being Function of bool X, bool X holds
Flip Flip f = f
proof
let X be set,
f be Function of bool X, bool X;
set g = Flip Flip f;
for x being Subset of X holds g.x = f.x
proof
let x be Subset of X;
g.x = ((Flip f).x`)` by FlipDef
.= (f.x``)`` by FlipDef
.= f.x;
hence thesis;
end;
hence thesis;
end;
registration let A be non empty set;
let f be universe-preserving Function of bool A, bool A;
cluster Flip f -> empty-preserving;
coherence
proof
f.A = A by UP;
hence thesis by EmFix;
end;
end;
registration let A be non empty set;
let f be empty-preserving Function of bool A, bool A;
cluster Flip f -> universe-preserving;
coherence
proof
f.{} = {} by EP;
hence thesis by Lm1;
end;
end;
theorem Flip4L:
for A being non empty set,
L, U being Function of bool A, bool A st
U = Flip L &
for X being Subset of A holds L.(L.X) c= L.X holds
for X being Subset of A holds U.X c= U.(U.X)
proof
let A be non empty set;
let L, U be Function of bool A, bool A;
assume that
A0: U = Flip L and
A1: for X being Subset of A holds L.(L.X) c= L.X;
let X be Subset of A;
A2: U.X = (L.X`)` by FlipDef,A0;
U.(U.X) = U.(L.X`)` by FlipDef,A0
.= (L.(L.X`)``)` by FlipDef,A0
.= (L.(L.X`))`;
hence thesis by A2,A1,SUBSET_1:12;
end;
begin :: Towards Topological Models of Rough Sets
definition let T be TopSpace;
func ClMap T -> Function of bool the carrier of T, bool the carrier of T
means :ClMapDef:
for X being Subset of T holds it.X = Cl X;
existence
proof
deffunc F(Subset of T) = Cl $1;
set X = the carrier of T;
ex g being Function of bool X, bool X st
for x being Element of bool X holds g.x = F(x) from FUNCT_2:sch 4; then
consider g being Function of bool X, bool X such that
A1: for x being Element of bool X holds g.x = F(x);
take g;
let x be Subset of X;
thus thesis by A1;
end;
uniqueness
proof
set X = the carrier of T;
let f1, f2 be Function of bool X, bool X such that
A1: for x being Subset of X holds f1.x = Cl x and
A2: for x being Subset of X holds f2.x = Cl x;
let x be Subset of X;
thus f1.x = Cl x by A1 .= f2.x by A2;
end;
func IntMap T -> Function of bool the carrier of T, bool the carrier of T
means :IntMapDef:
for X being Subset of T holds
it.X = Int X;
existence
proof
deffunc F(Subset of T) = Int $1;
set X = the carrier of T;
ex g being Function of bool X, bool X st
for x being Element of bool X holds g.x = F(x) from FUNCT_2:sch 4; then
consider g being Function of bool X, bool X such that
A1: for x being Element of bool X holds g.x = F(x);
take g;
let x be Subset of X;
thus thesis by A1;
end;
uniqueness
proof
set X = the carrier of T;
let f1, f2 be Function of bool X, bool X such that
A1: for x being Subset of X holds f1.x = Int x and
A2: for x being Subset of X holds f2.x = Int x;
let x be Subset of X;
thus f1.x = Int x by A1 .= f2.x by A2;
end;
end;
definition let T be TopSpace;
let f be Function of bool the carrier of T, bool the carrier of T;
attr f is closed-valued means
for X being Subset of T holds f.X is closed;
attr f is open-valued means
for X being Subset of T holds f.X is open;
end;
registration let T be TopSpace;
cluster ClMap T -> closed-valued;
coherence
proof
let X be Subset of T;
(ClMap T).X = Cl X by ClMapDef;
hence thesis;
end;
cluster IntMap T -> open-valued;
coherence
proof
let X be Subset of T;
(IntMap T).X = Int X by IntMapDef;
hence thesis;
end;
end;
registration let T be TopSpace;
cluster closed-valued
for Function of bool the carrier of T, bool the carrier of T;
existence
proof
take ClMap T;
thus thesis;
end;
cluster open-valued
for Function of bool the carrier of T, bool the carrier of T;
existence
proof
take IntMap T;
thus thesis;
end;
end;
theorem EqFlips:
for T being TopSpace holds
Flip ClMap T = IntMap T
proof
let T be TopSpace;
set f = Flip ClMap T, g = IntMap T;
for x being Subset of T holds f.x = g.x
proof
let x be Subset of T;
A1: (Int x)` = (Cl x`) by TDLAT_3:2;
f.x = ((ClMap T).x`)` by FlipDef
.= (Cl x`)` by ClMapDef
.= g.x by IntMapDef,A1;
hence thesis;
end;
hence thesis;
end;
theorem
for T being TopSpace holds
Flip IntMap T = ClMap T
proof
let T be TopSpace;
Flip Flip ClMap T = Flip IntMap T by EqFlips;
hence thesis by FlInv;
end;
registration let T be non empty TopSpace;
cluster ClMap T -> empty-preserving universe-preserving;
coherence
proof
set f = ClMap T;
A1: f.{}T = Cl {}T by ClMapDef .= {}T by PRE_TOPC:22;
f. [#]T = Cl [#]T by ClMapDef .= [#]T by PRE_TOPC:22;
hence thesis by A1;
end;
cluster IntMap T -> empty-preserving universe-preserving;
coherence
proof
set f = IntMap T;
A1: f.{}T = Int {}T by IntMapDef .= {}T;
f. [#]T = Int [#]T by IntMapDef .= [#]T by TOPS_1:15;
hence thesis by A1;
end;
end;
begin :: Formalization of Zhu's Paper
:: General Finite Relations
theorem FlUA:
for R being non empty RelStr holds
Flip UAp R = LAp R
proof
let R be non empty RelStr;
set f = Flip UAp R, g = LAp R;
for x being Subset of R holds f.x = g.x
proof
let x be Subset of R;
f.x = ((UAp R).x`)` by FlipDef
.= Lap x by DefU
.= LAp x by Mu2
.= g.x by DefL;
hence thesis;
end;
hence thesis;
end;
theorem FlLA:
for R being non empty RelStr holds
Flip LAp R = UAp R
proof
let R be non empty RelStr;
Flip UAp R = LAp R by FlUA;
hence thesis by FlInv;
end;
theorem Tw1U: :: Proposition 1 2H 4H
for A being non empty finite set,
U being Function of bool A, bool A st
U.{} = {} &
(for X, Y being Subset of A holds U.(X \/ Y) = U.X \/ U.Y) holds
ex R being non empty finite RelStr st
the carrier of R = A & U = UAp R
proof
let A be non empty finite set;
let L be Function of bool A, bool A;
assume that
A1: L.{} = {} and
A2: for X, Y being Subset of A holds L.(X \/ Y) = L.X \/ L.Y;
defpred P[set,set] means $1 in L.{$2};
consider R being Relation of A such that
B1: for x, y being Element of A holds
[x,y] in R iff P[x,y] from RELSET_1:sch 2;
reconsider RR = RelStr (#A, R#) as non empty finite RelStr;
take RR;
G1: for y be Element of RR, Y be Subset of RR st Y = {y} holds UAp Y = L.Y
proof
let y be Element of RR, Y be Subset of RR;
assume
A0: Y = {y};
thus UAp Y c= L.Y
proof
let x be element; assume x in UAp Y; then
consider a being Element of RR such that
A1: a = x & Class (the InternalRel of RR, a) meets Y;
consider z being element such that
H1: z in Class (the InternalRel of RR, a) & z in Y by A1,XBOOLE_0:3;
z = y by H1,TARSKI:def 1,A0; then
[x,y] in R by A1,H1,EQREL_1:18;
hence thesis by A0,B1,A1;
end;
let x be element;
assume
C1: x in L.Y;
KK: y in Y by TARSKI:def 1,A0;
a: L.Y in bool A by FUNCT_2:5; then
[x,y] in R by B1,C1,A0; then
y in Class (R, x) by EQREL_1:18; then
Class (the InternalRel of RR, x) meets Y by KK,XBOOLE_0:3;
hence thesis by a,C1;
end;
dom L = bool A by FUNCT_2:def 1; then
L1: dom UAp RR = dom L by FUNCT_2:def 1;
for x being element st x in dom UAp RR holds (UAp RR).x = L.x
proof
let x be element;
assume
p: x in dom UAp RR;
per cases;
suppose x <> {}; then
reconsider X = x as finite non empty Subset of RR by p;
defpred P[finite non empty Subset of RR] means (UAp RR).$1 = L.$1;
S1: for x being Element of RR st x in X holds P[{x}]
proof
let x be Element of RR;
assume x in X;
set I = {x};
(UAp RR).I = UAp I by DefU .= L.I by G1;
hence thesis;
end;
S2: for x being Element of RR,
B being non empty finite Subset of RR
st x in X & B c= X & not x in B & P[B] holds P[B \/ {x}]
proof
let x be Element of RR, B be non empty finite Subset of RR;
assume x in X & B c= X & not x in B & P[B]; then
Z1: UAp B = L.B by DefU;
set I = {x};
(UAp RR).(B \/ {x}) = UAp (B \/ I) by DefU
.= (UAp B) \/ (UAp I) by P24H
.= (L.B) \/ L.I by G1,Z1
.= L.(B \/ I) by A2;
hence thesis;
end;
P[X] from CHAIN_1:sch 2(S1,S2);
hence thesis;
end;
suppose
Q: x = {};
UAp {}RR = L.{} by A1;
hence thesis by DefU,Q;
end;
end;
hence thesis by L1,FUNCT_1:2;
end;
theorem Tw1: :: Proposition 1 1L 4L
for A being non empty finite set,
L being Function of bool A, bool A st
L.A = A &
(for X, Y being Subset of A holds L.(X /\ Y) = L.X /\ L.Y) holds
ex R being non empty finite RelStr st
the carrier of R = A & L = LAp R
proof
let A be non empty finite set,
L be Function of bool A, bool A;
assume that
A1: L.A = A and
A2: for X, Y being Subset of A holds L.(X /\ Y) = L.X /\ L.Y;
set U = Flip L;
A3: U.{} = {} by EmFix,A1;
A4: for X, Y being Subset of A holds U.(X \/ Y) = U.X \/ U.Y by FlSum,A2;
consider R being non empty finite RelStr such that
B1: the carrier of R = A & U = UAp R by Tw1U,A3,A4;
take R;
L = Flip UAp R by FlInv,B1;
hence thesis by B1,FlUA;
end;
:: Serial Relations
theorem Tw2: :: Proposition 2 1L 4L 2L
for A being non empty finite set,
L being Function of bool A, bool A st
L.A = A &
L.{} = {} &
(for X, Y being Subset of A holds L.(X /\ Y) = L.X /\ L.Y) holds
ex R being non empty serial RelStr st
the carrier of R = A & L = LAp R
proof
let A be non empty finite set;
let L be Function of bool A, bool A;
assume that
A1: L.A = A and
a1: L.{} = {} and
a2: for X, Y being Subset of A holds L.(X /\ Y) = L.X /\ L.Y;
consider R being non empty finite RelStr such that
A2: the carrier of R = A & L = LAp R by Tw1,a2,A1;
for x being element st x in the carrier of R
ex y being element st
y in the carrier of R & [x,y] in the InternalRel of R
proof
let x be element;
assume
BB: x in the carrier of R;
b3: (LAp R).{} = LAp {}R by DefL
.= { y where y is Element of R :
Class (the InternalRel of R, y) c= {} };
for y being Element of R holds Class (the InternalRel of R, y) <> {}
proof
let y be Element of R;
assume Class (the InternalRel of R, y) = {}; then
y in { y where y is Element of R :
Class (the InternalRel of R, y) c= {} };
hence contradiction by b3,A2,a1;
end; then
Class (the InternalRel of R, x) <> {} by BB; then
consider t be element such that
B4: t in Im(the InternalRel of R,x) by XBOOLE_0:def 1;
B5: [x,t] in the InternalRel of R by B4,RELAT_1:169; then
t in rng the InternalRel of R by BB,RELSET_1:25;
hence thesis by B5;
end; then
R is serial by Def0;
hence thesis by A2;
end;
theorem Tw2U: :: Proposition 2 1H 4H 2H
for A being non empty finite set,
U being Function of bool A, bool A st
U.A = A &
U.{} = {} &
(for X, Y being Subset of A holds U.(X \/ Y) = U.X \/ U.Y) holds
ex R being non empty finite serial RelStr st
the carrier of R = A & U = UAp R
proof
let A be non empty finite set;
let U be Function of bool A,bool A;
assume that
A0: U.A = A and
a1: U.{} = {} and
a2: for X, Y being Subset of A holds U.(X \/ Y) = U.X \/ U.Y;
consider R being non empty finite RelStr such that
A1: the carrier of R = A & U = UAp R by Tw1U,a1,a2;
for x being element st x in the carrier of R
ex y being element st
y in the carrier of R & [x,y] in the InternalRel of R
proof
let x be element;
assume
B1: x in the carrier of R;
reconsider Z = [#]A as Subset of R by A1;
UAp Z = Z by A1,A0,DefU; then
consider t being Element of R such that
B4: t = x & Class (the InternalRel of R,t) meets [#]A by B1,A1;
Class (the InternalRel of R,t) <> {} by B4; then
consider s being element such that
B5: s in Class (the InternalRel of R,t) by XBOOLE_0:def 1;
[t,s] in the InternalRel of R by B5,RELAT_1:169; then
[x,s] in the InternalRel of R & s in rng the InternalRel of R
by XTUPLE_0:def 13,B4;
hence thesis;
end; then
R is serial by Def0;
hence thesis by A1;
end;
theorem Tw3: :: Proposition 3 1L 4L 8LH
for A being non empty finite set,
L being Function of bool A, bool A st
L.A = A &
(for X being Subset of A holds L.X c= (L.(X`))`) &
(for X, Y being Subset of A holds L.(X /\ Y) = L.X /\ L.Y) holds
ex R being non empty finite serial RelStr st
the carrier of R = A & L = LAp R
proof
let A be non empty finite set;
let L be Function of bool A,bool A;
assume that
A0: L.A = A and
a1: for X being Subset of A holds L.X c= (L.(X`))` and
a2: for X, Y being Subset of A holds L.(X /\ Y) = L.X /\ L.Y;
consider R being non empty finite RelStr such that
A1: the carrier of R = A & L = LAp R by Tw1,A0,a2;
set XX = {}A;
X2: (L.(XX`)) = A by A0; then
x1: L.{} c= ([#]A)` by a1;
for x be element st x in the carrier of R
ex y being element st
y in the carrier of R & [x,y] in the InternalRel of R
proof
let x be element;
assume
B2: x in the carrier of R;
reconsider Z = [#]A as Subset of R by A1;
bb: (LAp R).{} = LAp {}R by DefL
.= { y where y is Element of R :
Class (the InternalRel of R, y) c= {} };
for y being Element of R holds Class (the InternalRel of R, y) <> {}
proof
let y be Element of R;
assume Class (the InternalRel of R, y) = {}; then
y in {z where z is Element of R :
Class (the InternalRel of R, z) c= {}};
hence contradiction by bb,A1,x1,X2;
end; then
Class (the InternalRel of R, x) <> {} by B2; then
consider t be element such that
B4: t in Im(the InternalRel of R,x) by XBOOLE_0:def 1;
B5: [x,t] in the InternalRel of R by B4,RELAT_1:169; then
t in rng the InternalRel of R by RELSET_1:25,B2;
hence thesis by B5;
end; then
R is serial by Def0;
hence thesis by A1;
end;
theorem Tw3U: :: Proposition 4 2H 4H 8LH
for A being non empty finite set,
U being Function of bool A, bool A st
U.{} = {} &
(for X being Subset of A holds (U.(X`))` c= U.X) &
(for X, Y being Subset of A holds U.(X \/ Y) = U.X \/ U.Y) holds
ex R being non empty serial RelStr st
the carrier of R = A & U = UAp R
proof
let A be non empty finite set;
let U be Function of bool A,bool A;
assume that
A0: U.{} = {} and
a1: for X being Subset of A holds (U.(X`))` c= U.X and
a2: for X, Y being Subset of A holds U.(X \/ Y) = U.X \/ U.Y;
consider R being non empty finite RelStr such that
A1: the carrier of R = A & U = UAp R by Tw1U,A0,a2;
for x being element st x in the carrier of R
ex y being element
st y in the carrier of R & [x,y] in the InternalRel of R
proof
let x be element;
assume
B0: x in the carrier of R;
reconsider Z = [#]A as Subset of R by A1;
set XX = [#]A;
(U.(XX`))` c= U.XX by a1; then
({}A)` c= U.XX by A0; then
x1: (Flip UAp R).{} = {} by EmFix,A1,XBOOLE_0:def 10;
bc: (LAp R).{} = LAp {}R by DefL
.= { y where y is Element of R :
Class (the InternalRel of R, y) c= {} };
for y being Element of R holds Class (the InternalRel of R, y) <> {}
proof
let y be Element of R;
assume Class (the InternalRel of R, y) = {}; then
y in {z where z is Element of R :
Class (the InternalRel of R, z) c= {}};
hence contradiction by bc,x1,FlUA;
end; then
Class (the InternalRel of R, x) <> {} by B0; then
consider t being element such that
B4: t in Im(the InternalRel of R,x) by XBOOLE_0:def 1;
B5: [x,t] in the InternalRel of R by B4,RELAT_1:169; then
t in rng the InternalRel of R by RELSET_1:25,B0;
hence thesis by B5;
end; then
R is serial by Def0;
hence thesis by A1;
end;
:: Reflexive binary relations
theorem :: Proposition 5 3L
for R being non empty reflexive RelStr,
X being Subset of R holds
LAp X c= X
proof
let R be non empty reflexive RelStr;
let X be Subset of R;
let y be element;
assume y in LAp X; then
consider z being Element of R such that
A1: z = y & Class (the InternalRel of R,z) c= X;
A2: z in field the InternalRel of R by help0;
A3: z in {z} by TARSKI:def 1;
[z,z] in the InternalRel of R by A2,RELAT_2:def 1,def 9; then
z in (the InternalRel of R) .: {z} by RELAT_1:def 13,A3;
hence thesis by A1;
end;
theorem :: Proposition 5 3H
for R being non empty reflexive RelStr,
X being Subset of R holds
X c= UAp X
proof
let R be non empty reflexive RelStr,
X be Subset of R;
let y be element;
assume
A0: y in X; then
y in Class (the InternalRel of R,y) by help3; then
Class (the InternalRel of R,y) meets X by A0,XBOOLE_0:def 4;
hence thesis by A0;
end;
theorem Prop5: :: Proposition 5 1H 4H 3H
for A being non empty finite set,
U being Function of bool A, bool A st
U.{} = {} &
(for X being Subset of A holds X c= U.X) &
(for X,Y being Subset of A holds U.(X \/ Y) = U.X \/ U.Y) holds
ex R being non empty finite reflexive RelStr st
the carrier of R = A & U = UAp R
proof
let A be non empty finite set;
let U be Function of bool A, bool A;
assume that
A0: U.{} = {} and
a1: for X being Subset of A holds X c= U.X and
a2: for X,Y being Subset of A holds U.(X \/ Y) = U.X \/ U.Y;
U.([#]A) c= [#]A & [#]A c= U.([#]A) by a1; then
U.A = A; then
consider R being non empty finite serial RelStr such that
A1: the carrier of R = A & U = UAp R by Tw2U,A0,a2;
for x being element st x in the carrier of R holds
[x,x] in the InternalRel of R
proof
let x be element;
assume
d: x in the carrier of R; then
dd: {x} is Subset of R by ZFMISC_1:31;
reconsider Z = {x} as Subset of R by d,ZFMISC_1:31;
D2: {x} c= U.({x}) by A1,dd,a1;
x in {x} by TARSKI:def 1; then
D3: x in U.({x}) by D2;
U.({x}) = UAp Z by DefU,A1
.= {y where y is Element of R :
Class (the InternalRel of R,y) meets Z}; then
consider t being Element of R such that
D4: t = x & Class (the InternalRel of R,t) meets Z by D3;
x in Class (the InternalRel of R,t)
proof
assume
E1: not x in Class (the InternalRel of R,t);
consider y being element such that
E2: y in Class (the InternalRel of R,t) /\ {x} by D4,XBOOLE_0:def 1;
y in Class (the InternalRel of R,t) & y in {x} by XBOOLE_0:def 4,E2;
hence contradiction by E1,TARSKI:def 1;
end;
hence thesis by D4,RELAT_1:169;
end;
then R is reflexive by ORDERS_2:def 2,RELAT_2:def 1;
hence thesis by A1;
end;
theorem :: Proposition 5 1L 4L 3L
for A being non empty finite set,
L being Function of bool A, bool A st
L.A = A &
(for X being Subset of A holds L.X c= X) &
(for X,Y being Subset of A holds L.(X /\ Y) = L.X /\ L.Y) holds
ex R being non empty finite reflexive RelStr st
the carrier of R = A & L = LAp R
proof
let A be non empty finite set;
let L be Function of bool A, bool A;
assume that
A0: L.A = A and
a1: for X being Subset of A holds L.X c= X and
a2: for X,Y being Subset of A holds L.(X /\ Y) = L.X /\ L.Y;
set U = Flip L;
N1: U.{} = {} by A0,EmFix;
N2: for X being Subset of A holds X c= U.X
proof
let X be Subset of A;
X`` c= (L.X`)` by a1,SUBSET_1:12;
hence thesis by FlipDef;
end;
for X,Y being Subset of A holds U.(X \/ Y) = U.X \/ U.Y
by a2,FlSum; then
consider R being non empty finite reflexive RelStr such that
A1: the carrier of R = A & U = UAp R by Prop5,N1,N2;
L = Flip UAp R by FlInv,A1; then
L = LAp R by FlUA;
hence thesis by A1;
end;
:: Mediate Relations
theorem ThU5H: :: Proposition 6 5H'
for R being non empty mediate RelStr,
X being Subset of R holds
UAp X c= UAp (UAp X)
proof
let R be non empty mediate RelStr;
let X be Subset of R;
let y be element;
assume y in UAp X; then
consider t being Element of R such that
A1: t = y & Class (the InternalRel of R,t) meets X;
ex w being element st
w in Class (the InternalRel of R,t) /\ X by A1,XBOOLE_0:def 1; then
consider w being Element of the carrier of R such that
a2: w in Class (the InternalRel of R,t) /\ X;
A2: w in Class (the InternalRel of R,t) & w in X by XBOOLE_0:def 4,a2; then
[t,w] in the InternalRel of R by RELAT_1:169; then
consider z being element such that
A3: z in the carrier of R & [t,z] in the InternalRel of R &
[z,w] in the InternalRel of R by DefM1,DefM2;
reconsider z as Element of R by A3;
A4: z in Class (the InternalRel of R,t) &
w in Class (the InternalRel of R,z) by A3,RELAT_1:169; then
Class (the InternalRel of R,z) meets X by A2,XBOOLE_0:def 4; then
aa: z in {x where x is Element of R : Class (the InternalRel of R,x) meets X};
A6: UAp {z} c= UAp (UAp X) by ThUzaw,aa,ZFMISC_1:31;
z in {z} by TARSKI:def 1; then
Class (the InternalRel of R,t) meets {z} by A4,XBOOLE_0:def 4; then
t in {x where x is Element of R :
Class (the InternalRel of R,x) meets {z} };
hence thesis by A1,A6;
end;
theorem :: Proposition 6 5L'
for R being non empty mediate RelStr,
X being Subset of R holds
LAp (LAp X) c= LAp X
proof
let R be non empty mediate RelStr;
let X be Subset of R;
A1: LAp (LAp X) = LAp ((LAp X)``)
.= (UAp (LAp (X``))`)` by Th8LH
.= (UAp ((UAp (X`))``))` by Th8LH
.= (UAp (UAp (X`)))`;
(UAp (X`))` = LAp (X``) by Th8LH
.= LAp X;
hence thesis by A1,SUBSET_1:12,ThU5H;
end;
theorem Prop7: :: Proposition 7 2H 4H 5H'
for A being non empty finite set,
U being Function of bool A, bool A st
U.{} = {} &
(for X being Subset of A holds U.X c= U.(U.X)) &
(for X,Y being Subset of A holds U.(X \/ Y) = U.X \/ U.Y) holds
ex R being non empty mediate finite RelStr st
the carrier of R = A & U = UAp R
proof
let A be non empty finite set;
let U be Function of bool A,bool A;
assume that
A0: U.{} = {} and
a1: for X being Subset of A holds U.X c= U.(U.X) and
a2: for X,Y being Subset of A holds U.(X \/ Y) = U.X \/ U.Y;
consider R being non empty finite RelStr such that
A2: the carrier of R = A & U = UAp R by Tw1U,A0,a2;
for x,y being element st
x in the carrier of R & y in the carrier of R holds
[x,y] in the InternalRel of R implies
ex z being element
st z in the carrier of R & [x,z] in the InternalRel of R &
[z,y] in the InternalRel of R
proof
let x,y be element;
assume
A00: x in the carrier of R & y in the carrier of R; then
reconsider Y = {y} as Subset of R by ZFMISC_1:31;
assume
A1: [x,y] in the InternalRel of R;
reconsider x as Element of R by A00;
y in Class (the InternalRel of R,x) & y in {y}
by A1,TARSKI:def 1,RELAT_1:169; then
Class (the InternalRel of R,x) meets {y} by XBOOLE_0:def 4; then
B1: x in UAp Y;
x in UAp (UAp Y)
proof
B3: x in U.Y by A2,DefU,B1;
x in U.(U.Y) by a1,TARSKI:def 3,A2,B3; then
x in U.(UAp Y) by DefU,A2;
hence thesis by DefU,A2;
end; then
consider t being Element of R such that
B4: t = x & Class (the InternalRel of R,t) meets UAp Y;
consider z being element such that
B5: z in Class (the InternalRel of R,t) /\ UAp Y by B4,XBOOLE_0:def 1;
reconsider Z = {z} as Subset of R by ZFMISC_1:31,B5;
Sa: z in {z} & z in Class (the InternalRel of R,t) & z in UAp Y
by B5,XBOOLE_0:def 4,TARSKI:def 1; then
Class (the InternalRel of R,t) meets {z} by XBOOLE_0:def 4; then
t in UAp Z; then
[t,z] in the InternalRel of R & [z,y] in the InternalRel of R
by Sa,A00,help7;
hence thesis by B4,B5;
end; then
R is mediate by DefM1;
hence thesis by A2;
end;
theorem :: Proposition 8 1L 4L 5L'
for A being non empty finite set,
L being Function of bool A, bool A st
L.A = A &
(for X being Subset of A holds L.(L.X) c= L.X) &
(for X,Y being Subset of A holds L.(X /\ Y) = L.X /\ L.Y) holds
ex R being non empty mediate finite RelStr st
the carrier of R = A & L = LAp R
proof
let A be non empty finite set;
let L be Function of bool A, bool A;
assume that
A0: L.A = A and
a1: for X being Subset of A holds L.(L.X) c= L.X and
a2: for X,Y being Subset of A holds L.(X /\ Y) = L.X /\ L.Y;
set U = Flip L;
T1: U.{} = {} by A0,EmFix;
T2: for X being Subset of A holds U.X c= U.(U.X) by Flip4L,a1;
for X,Y being Subset of A holds U.(X \/ Y) = U.X \/ U.Y by FlSum,a2; then
consider R being non empty mediate finite RelStr such that
A2: the carrier of R = A & U = UAp R by Prop7,T1,T2;
take R;
L = Flip UAp R by FlInv,A2;
hence thesis by A2,FlUA;
end;
:: Corollaries
theorem :: Corollary 1
for A being non empty finite set,
L being Function of bool A, bool A st
L.A = A &
(for X, Y being Subset of A holds L.(X /\ Y) = L.X /\ L.Y) holds
(for X being Subset of A holds L.X c= (L.(X`))`)
iff
L.{} = {}
proof
let A be non empty finite set;
let L be Function of bool A,bool A;
assume that
A0: L.A = A and
a1: for X, Y being Subset of A holds L.(X /\ Y) = L.X /\ L.Y;
thus (for X being Subset of A holds L.X c= (L.(X`))` ) implies L.{} = {}
proof
assume for X being Subset of A holds L.X c= (L.(X`))`; then
consider R being non empty serial finite RelStr such that
A2: the carrier of R = A & L = LAp R by A0,Tw3,a1;
L.{} = LAp {}R by DefL,A2;
hence thesis;
end;
assume L.{} = {}; then
consider R being non empty serial RelStr such that
B2: the carrier of R = A & L = LAp R by A0,Tw2,a1;
let X be Subset of A;
reconsider Xa = X as Subset of R by B2;
set U = Flip L;
BB: U = UAp R by B2,FlLA;
LAp Xa c= UAp Xa by Th9LH; then
LAp Xa c= (UAp R).X by DefU; then
(LAp R).X c= (UAp R).X by DefL;
hence thesis by FlipDef,B2,BB;
end;
theorem :: Corollary 2
for A being non empty finite set,
U being Function of bool A, bool A st
U.{} = {} &
(for X,Y being Subset of A holds U.(X \/ Y) = U.X \/ U.Y) holds
(for X being Subset of A holds (U.(X`))` c= U.X)
iff
U.A = A
proof
let A be non empty finite set;
let U be Function of bool A,bool A;
assume that
A0: U.{} = {} and
a1: for X,Y being Subset of A holds U.(X \/ Y) = U.X \/ U.Y;
thus (for X being Subset of A holds (U.(X`))` c= U.X) implies U.A = A
proof
assume for X being Subset of A holds (U.(X`))` c= U.X; then
consider R being non empty serial RelStr such that
B2: the carrier of R = A & U = UAp R by Tw3U,A0,a1;
(UAp R).[#]R = UAp [#]R by DefU;
hence thesis by B2;
end;
assume U.A = A; then
consider R being non empty finite serial RelStr such that
B2: the carrier of R = A & U = UAp R by A0,Tw2U,a1;
let X be Subset of A;
reconsider Xa = X as Subset of R by B2;
set L = Flip U;
BB: L = LAp R by B2,FlUA;
LAp Xa c= UAp Xa by Th9LH; then
LAp Xa c= (UAp R).X by DefU; then
(LAp R).X c= (UAp R).X by DefL;
hence thesis by FlipDef,B2,BB;
end;