:: Formalizing Two Generalized Approximation Operators
:: by Adam Grabowski and Micha{\l} Sielwiesiuk
::
:: Copyright (c) 2018-2019 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 :MapRefl: :: ROUGHS_5:def 1
for u being Element of R holds u in I . u;
end;

:: deftheorem MapRefl 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 b1 being Function of R,(bool R) st
for x being Element of R holds b1 . x = {x}
proof end;
uniqueness
for b1, b2 being Function of R,(bool R) st ( for x being Element of R holds b1 . x = {x} ) & ( for x being Element of R holds b2 . x = {x} ) holds
b1 = b2
proof end;
correctness
;
end;

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

registration
let R be non empty set ;
coherence
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 b1 being Function of the carrier of R,(bool the carrier of R) st
for x being Element of R holds b1 . x = Coim ( the InternalRel of R,x)
proof end;
uniqueness
for b1, b2 being Function of the carrier of R,(bool the carrier of R) st ( for x being Element of R holds b1 . x = Coim ( the InternalRel of R,x) ) & ( for x being Element of R holds b2 . x = Coim ( the InternalRel of R,x) ) holds
b1 = b2
proof end;
correctness
;
end;

:: deftheorem DefUnc defines UncertaintyMap ROUGHS_5:def 3 :
for R being non empty RelStr
for b2 being Function of the carrier of R,(bool the carrier of R) holds
( b2 = UncertaintyMap R iff for x being Element of R holds b2 . 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 () . 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 b1 being Function of the carrier of R,(bool the carrier of R) st
for u being Element of R holds b1 . u = Im ( the InternalRel of R,u)
proof end;
uniqueness
for b1, b2 being Function of the carrier of R,(bool the carrier of R) st ( for u being Element of R holds b1 . u = Im ( the InternalRel of R,u) ) & ( for u being Element of R holds b2 . u = Im ( the InternalRel of R,u) ) holds
b1 = b2
proof end;
end;

:: deftheorem DefTau defines tau ROUGHS_5:def 4 :
for R being non empty RelStr
for b2 being Function of the carrier of R,(bool the carrier of R) holds
( b2 = tau R iff for u being Element of R holds b2 . 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 b1 being map of R st
for x being Subset of R holds b1 . x = { u where u is Element of R : f . u meets x }
proof end;
uniqueness
for b1, b2 being map of R st ( for x being Subset of R holds b1 . x = { u where u is Element of R : f . u meets x } ) & ( for x being Subset of R holds b2 . x = { u where u is Element of R : f . u meets x } ) holds
b1 = b2
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 b3 being map of R holds
( b3 = ff_0 f iff for x being Subset of R holds b3 . 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 :F0Unc: :: 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 :F1Unc: :: ROUGHS_5:def 7
ff_0 ();
coherence
ff_0 () is map of R
;
end;

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

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

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

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 )

proof end;

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);
coherence 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 () . u = () . 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 : () . 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 () . u = () . 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 () . 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 ;
coherence by ReflUnc;
coherence 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 (() .: ([#] 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 ;
coherence by F0Mono;
coherence 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)
proof end;

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

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

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

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

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

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

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