:: Formalizing Two Generalized Approximation Operators
:: by Adam Grabowski and Micha{\l} Sielwiesiuk
::
:: Received June 29, 2018
:: Copyright (c) 2018-2021 Association of Mizar Users

definition

let R be non empty set ;
let I be Function of R,(bool R);

attr I is map-reflexive means :: ROUGHS_5:def 1
for u being Element of R holds u in I . u;

end;

:: deftheorem defines map-reflexive ROUGHS_5:def 1 :
for R being non empty set
for I being Function of R,(bool R) holds
( I is map-reflexive iff for u being Element of R holds u in I . u );

definition

let R be non empty set ;

func singleton R -> Function of R,(bool R) means :SingleFunc: :: ROUGHS_5:def 2
for x being Element of R holds it . x = {x};

existence
ex b₁ being Function of R,(bool R) st
for x being Element of R holds b₁ . x = {x}

proof end;

uniqueness
for b₁, b₂ being Function of R,(bool R) st ( for x being Element of R holds b₁ . x = {x} ) & ( for x being Element of R holds b₂ . x = {x} ) holds
b₁ = b₂

proof end;

correctness
;

end;

:: deftheorem SingleFunc defines singleton ROUGHS_5:def 2 :
for R being non empty set
for b₂ being Function of R,(bool R) holds
( b₂ = singleton R iff for x being Element of R holds b₂ . x = {x} );

registration

let R be non empty set ;

cluster singleton R -> map-reflexive ;

coherence
singleton R is map-reflexive

proof end;

end;

theorem :: ROUGHS_5:1

for R being non empty RelStr
for I being Function of the carrier of R,(bool the carrier of R) st I is map-reflexive holds
the carrier of R = union (I .: ([#] R))

proof end;

theorem LApId: :: ROUGHS_5:2

for R being non empty reflexive RelStr holds LAp R cc= id (bool the carrier of R)

proof end;

theorem :: ROUGHS_5:3

for R being non empty reflexive RelStr holds id (bool the carrier of R) cc= UAp R

proof end;

theorem :: ROUGHS_5:4

for R being non empty RelStr
for f being map of R
for x, y being Subset of R holds Flip (Flip f) = f by ROUGHS_2:23;

::: $f^d$

theorem FlipCompose: :: ROUGHS_5:5

for R being non empty RelStr
for f, g being map of R holds Flip (f * g) = (Flip f) * (Flip g)

proof end;

theorem :: ROUGHS_5:6

for R being non empty RelStr
for f being map of R holds
( f . {} = {} iff (Flip f) . the carrier of R = the carrier of R )

proof end;

definition

let R be non empty RelStr ;

func UncertaintyMap R -> Function of the carrier of R,(bool the carrier of R) means :DefUnc: :: ROUGHS_5:def 3
for x being Element of R holds it . x = Coim ( the InternalRel of R,x);

existence
ex b₁ being Function of the carrier of R,(bool the carrier of R) st
for x being Element of R holds b₁ . x = Coim ( the InternalRel of R,x)

proof end;

uniqueness
for b₁, b₂ being Function of the carrier of R,(bool the carrier of R) st ( for x being Element of R holds b₁ . x = Coim ( the InternalRel of R,x) ) & ( for x being Element of R holds b₂ . x = Coim ( the InternalRel of R,x) ) holds
b₁ = b₂

proof end;

correctness
;

end;

:: deftheorem DefUnc defines UncertaintyMap ROUGHS_5:def 3 :
for R being non empty RelStr
for b₂ being Function of the carrier of R,(bool the carrier of R) holds
( b₂ = UncertaintyMap R iff for x being Element of R holds b₂ . x = Coim ( the InternalRel of R,x) );

theorem For3: :: ROUGHS_5:7

for R being non empty RelStr
for w, u being Element of R holds
( [w,u] in the InternalRel of R iff w in (UncertaintyMap R) . u )

proof end;

definition

let R be non empty RelStr ;

func tau R -> Function of the carrier of R,(bool the carrier of R) means :DefTau: :: ROUGHS_5:def 4
for u being Element of R holds it . u = Im ( the InternalRel of R,u);

existence
ex b₁ being Function of the carrier of R,(bool the carrier of R) st
for u being Element of R holds b₁ . u = Im ( the InternalRel of R,u)

proof end;

uniqueness
for b₁, b₂ being Function of the carrier of R,(bool the carrier of R) st ( for u being Element of R holds b₁ . u = Im ( the InternalRel of R,u) ) & ( for u being Element of R holds b₂ . u = Im ( the InternalRel of R,u) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem DefTau defines tau ROUGHS_5:def 4 :
for R being non empty RelStr
for b₂ being Function of the carrier of R,(bool the carrier of R) holds
( b₂ = tau R iff for u being Element of R holds b₂ . u = Im ( the InternalRel of R,u) );

theorem ImCoim: :: ROUGHS_5:8

for R being non empty RelStr
for u, w being Element of R holds
( u in Im ( the InternalRel of R,w) iff w in Coim ( the InternalRel of R,u) )

proof end;

theorem For3A: :: ROUGHS_5:9

for R being non empty RelStr
for w, u being Element of R holds
( [w,u] in the InternalRel of R iff u in (tau R) . w )

proof end;

:: General version of the induced mapping

definition

let R be non empty RelStr ;
let f be Function of the carrier of R,(bool the carrier of R);

func ff_0 f -> map of R means :Defff: :: ROUGHS_5:def 5
for x being Subset of R holds it . x = { u where u is Element of R : f . u meets x } ;

existence
ex b₁ being map of R st
for x being Subset of R holds b₁ . x = { u where u is Element of R : f . u meets x }

proof end;

uniqueness
for b₁, b₂ being map of R st ( for x being Subset of R holds b₁ . x = { u where u is Element of R : f . u meets x } ) & ( for x being Subset of R holds b₂ . x = { u where u is Element of R : f . u meets x } ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Defff defines ff_0 ROUGHS_5:def 5 :
for R being non empty RelStr
for f being Function of the carrier of R,(bool the carrier of R)
for b₃ being map of R holds
( b₃ = ff_0 f iff for x being Subset of R holds b₃ . x = { u where u is Element of R : f . u meets x } );

definition

let R be non empty RelStr ;

func f_0 R -> map of R equals :: ROUGHS_5:def 6
ff_0 (tau R);

coherence
ff_0 (tau R) is map of R ;

func f_1 R -> map of R equals :: ROUGHS_5:def 7
ff_0 (UncertaintyMap R);

coherence
ff_0 (UncertaintyMap R) is map of R ;

end;

:: deftheorem defines f_0 ROUGHS_5:def 6 :
for R being non empty RelStr holds f_0 R = ff_0 (tau R);

:: deftheorem defines f_1 ROUGHS_5:def 7 :
for R being non empty RelStr holds f_1 R = ff_0 (UncertaintyMap R);

theorem UncEqTau: :: ROUGHS_5:10

for R being non empty RelStr st the InternalRel of R is symmetric holds
UncertaintyMap R = tau R

proof end;

theorem :: ROUGHS_5:11

for R being non empty RelStr st the InternalRel of R is symmetric holds
f_0 R = f_1 R by UncEqTau;

Lemacik: for R being non empty RelStr
for a, b being object
for RR being Relation of the carrier of R st [a,b] in RR holds
( a is Element of R & b is Element of R )
by ZFMISC_1:87;

theorem :: ROUGHS_5:12

for R being non empty RelStr holds
( the InternalRel of R is symmetric iff for u, v being Element of R st u in (tau R) . v holds
v in (tau R) . u )

proof end;

theorem UApF0: :: ROUGHS_5:13

for R being non empty RelStr holds f_0 R = UAp R

proof end;

theorem FlipLAp: :: ROUGHS_5:14

for R being non empty RelStr holds Flip (f_0 R) = LAp R

proof end;

theorem :: ROUGHS_5:15

for R being Approximation_Space
for x being Subset of R holds (f_0 R) . x is exact

proof end;

theorem :: ROUGHS_5:16

for R being non empty RelStr st the InternalRel of R is total & the InternalRel of R is reflexive holds
id (bool the carrier of R) cc= f_0 R

proof end;

theorem :: ROUGHS_5:17

for R being non empty RelStr st R is reflexive holds
Flip (f_0 R) cc= id (bool the carrier of R)

proof end;

theorem :: ROUGHS_5:18

for R being non empty RelStr st the InternalRel of R is total & the InternalRel of R is reflexive holds
id (bool the carrier of R) cc= f_1 R

proof end;

theorem Proph: :: ROUGHS_5:19

for R being non empty RelStr
for f being Function of the carrier of R,(bool the carrier of R) holds (ff_0 f) . {} = {}

proof end;

registration

let R be non empty RelStr ;
let f be Function of the carrier of R,(bool the carrier of R);

cluster ff_0 f -> empty-preserving ;

coherence
ff_0 f is empty-preserving by Proph;

end;

theorem :: ROUGHS_5:20

for R being non empty RelStr holds (f_0 R) . {} = {}

proof end;

theorem :: ROUGHS_5:21

for R being non empty RelStr holds (f_1 R) . {} = {}

proof end;

registration

let R be non empty reflexive RelStr ;

cluster the InternalRel of R -> reflexive total ;

coherence
( the InternalRel of R is total & the InternalRel of R is reflexive ) ;

end;

theorem :: ROUGHS_5:22

for R being non empty RelStr
for f being Function of the carrier of R,(bool the carrier of R) st f is map-reflexive holds
(ff_0 f) . the carrier of R = the carrier of R

proof end;

theorem :: ROUGHS_5:23

for R being non empty RelStr st the InternalRel of R is reflexive & the InternalRel of R is total holds
(f_0 R) . the carrier of R = the carrier of R

proof end;

theorem :: ROUGHS_5:24

for R being non empty RelStr st the InternalRel of R is reflexive & the InternalRel of R is total holds
(f_1 R) . the carrier of R = the carrier of R

proof end;

theorem :: ROUGHS_5:25

for R being non empty RelStr
for f being Function of the carrier of R,(bool the carrier of R)
for u, w being Element of R
for x being Subset of R st f . u = f . w holds
( u in (ff_0 f) . x iff w in (ff_0 f) . x )

proof end;

theorem :: ROUGHS_5:26

for R being non empty RelStr
for u, w being Element of R
for x being Subset of R st (UncertaintyMap R) . u = (UncertaintyMap R) . w holds
( u in (f_1 R) . x iff w in (f_1 R) . x )

proof end;

theorem :: ROUGHS_5:27

for R being non empty RelStr
for u, w being Element of R
for x being Subset of R st (tau R) . u = (tau R) . w holds
( u in (f_0 R) . x iff w in (f_0 R) . x )

proof end;

theorem FlipFF: :: ROUGHS_5:28

for R being non empty RelStr
for f being Function of the carrier of R,(bool the carrier of R)
for x being Subset of R holds (Flip (ff_0 f)) . x = { w where w is Element of R : f . w c= x }

proof end;

theorem FlipF0: :: ROUGHS_5:29

for R being non empty RelStr
for x being Subset of R holds (Flip (f_0 R)) . x = { w where w is Element of R : (tau R) . w c= x }

proof end;

theorem FlipF1: :: ROUGHS_5:30

for R being non empty RelStr
for x being Subset of R holds (Flip (f_1 R)) . x = { w where w is Element of R : (UncertaintyMap R) . w c= x }

proof end;

theorem :: ROUGHS_5:31

for R being non empty RelStr
for f being Function of the carrier of R,(bool the carrier of R)
for u, w being Element of R
for x being Subset of R st f . u = f . w holds
( u in (Flip (ff_0 f)) . x iff w in (Flip (ff_0 f)) . x )

proof end;

theorem :: ROUGHS_5:32

for R being non empty RelStr
for u, w being Element of R
for x being Subset of R st (tau R) . u = (tau R) . w holds
( u in (Flip (f_0 R)) . x iff w in (Flip (f_0 R)) . x )

proof end;

theorem :: ROUGHS_5:33

for R being non empty RelStr
for u, w being Element of R
for x being Subset of R st (UncertaintyMap R) . u = (UncertaintyMap R) . w holds
( u in (Flip (f_1 R)) . x iff w in (Flip (f_1 R)) . x )

proof end;

theorem ReflUnc: :: ROUGHS_5:34

for R being non empty RelStr st R is reflexive holds
for w being Element of R holds w in (UncertaintyMap R) . w

proof end;

theorem ReflTau: :: ROUGHS_5:35

for R being non empty RelStr st R is reflexive holds
for w being Element of R holds w in (tau R) . w

proof end;

registration

let R be non empty reflexive RelStr ;

cluster UncertaintyMap R -> map-reflexive ;

coherence
UncertaintyMap R is map-reflexive by ReflUnc;

cluster tau R -> map-reflexive ;

coherence
tau R is map-reflexive by ReflTau;

end;

theorem :: ROUGHS_5:36

for R being non empty RelStr st R is reflexive holds
Flip (f_1 R) cc= id (bool the carrier of R)

proof end;

theorem :: ROUGHS_5:37

for R being non empty RelStr holds
( (f_0 R) * (f_0 R) = f_0 R iff (Flip (f_0 R)) * (Flip (f_0 R)) = Flip (f_0 R) )

proof end;

theorem :: ROUGHS_5:38

for R being non empty RelStr st R is reflexive holds
union ((UncertaintyMap R) .: ([#] R)) = the carrier of R

proof end;

F0Mono: for R being non empty RelStr holds f_0 R is c=-monotone

proof end;

F1Mono: for R being non empty RelStr holds f_1 R is c=-monotone

proof end;

registration

let R be non empty RelStr ;

cluster f_0 R -> c=-monotone ;

coherence
f_0 R is c=-monotone by F0Mono;

cluster f_1 R -> c=-monotone ;

coherence
f_1 R is c=-monotone by F1Mono;

end;

theorem FlipMono: :: ROUGHS_5:39

for R being non empty RelStr
for f being map of R st f is c=-monotone holds
Flip f is c=-monotone

proof end;

theorem :: ROUGHS_5:40

for R being non empty RelStr holds Flip (f_0 R) is c=-monotone by FlipMono;

theorem :: ROUGHS_5:41

for R being non empty RelStr holds Flip (f_1 R) is c=-monotone by FlipMono;

theorem Propj: :: ROUGHS_5:42

for R being non empty RelStr
for f being Function of the carrier of R,(bool the carrier of R)
for x, y being Subset of R holds (ff_0 f) . (x \/ y) = ((ff_0 f) . x) \/ ((ff_0 f) . y)

proof end;

theorem :: ROUGHS_5:43

for R being non empty RelStr
for x, y being Subset of R holds (f_0 R) . (x \/ y) = ((f_0 R) . x) \/ ((f_0 R) . y) by Propj;

theorem :: ROUGHS_5:44

for R being non empty RelStr
for x, y being Subset of R holds (f_1 R) . (x \/ y) = ((f_1 R) . x) \/ ((f_1 R) . y) by Propj;

theorem Propk: :: ROUGHS_5:45

for R being non empty RelStr
for f being Function of the carrier of R,(bool the carrier of R)
for x, y being Subset of R holds ((Flip (ff_0 f)) . x) \/ ((Flip (ff_0 f)) . y) c= (Flip (ff_0 f)) . (x \/ y)

proof end;

theorem :: ROUGHS_5:46

for R being non empty RelStr
for x, y being Subset of R holds ((Flip (f_0 R)) . x) \/ ((Flip (f_0 R)) . y) c= (Flip (f_0 R)) . (x \/ y) by Propk;

theorem :: ROUGHS_5:47

for R being non empty RelStr
for x, y being Subset of R holds ((Flip (f_1 R)) . x) \/ ((Flip (f_1 R)) . y) c= (Flip (f_1 R)) . (x \/ y) by Propk;

theorem Propl: :: ROUGHS_5:48

for R being non empty RelStr
for f being Function of the carrier of R,(bool the carrier of R)
for x, y being Subset of R holds (ff_0 f) . (x /\ y) c= ((ff_0 f) . x) /\ ((ff_0 f) . y)

proof end;

theorem :: ROUGHS_5:49

for R being non empty RelStr
for x, y being Subset of R holds (f_0 R) . (x /\ y) c= ((f_0 R) . x) /\ ((f_0 R) . y) by Propl;

theorem :: ROUGHS_5:50

for R being non empty RelStr
for x, y being Subset of R holds (f_1 R) . (x /\ y) c= ((f_1 R) . x) /\ ((f_1 R) . y) by Propl;

theorem Propm: :: ROUGHS_5:51

for R being non empty RelStr
for f being Function of the carrier of R,(bool the carrier of R)
for x, y being Subset of R holds ((Flip (ff_0 f)) . x) /\ ((Flip (ff_0 f)) . y) = (Flip (ff_0 f)) . (x /\ y)

proof end;

theorem :: ROUGHS_5:52

for R being non empty RelStr
for x, y being Subset of R holds ((Flip (f_0 R)) . x) /\ ((Flip (f_0 R)) . y) = (Flip (f_0 R)) . (x /\ y) by Propm;

theorem :: ROUGHS_5:53

for R being non empty RelStr
for x, y being Subset of R holds ((Flip (f_1 R)) . x) /\ ((Flip (f_1 R)) . y) = (Flip (f_1 R)) . (x /\ y) by Propm;