:: by Adam Grabowski and Micha{\l} Sielwiesiuk

::

:: Received June 29, 2018

:: Copyright (c) 2018-2021 Association of Mizar Users

:: 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 );

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 ;

ex b_{1} being Function of R,(bool R) st

for x being Element of R holds b_{1} . x = {x}

for b_{1}, b_{2} being Function of R,(bool R) st ( for x being Element of R holds b_{1} . x = {x} ) & ( for x being Element of R holds b_{2} . x = {x} ) holds

b_{1} = b_{2}

;

end;
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 for x being Element of R holds it . x = {x};

ex b

for x being Element of R holds b

proof end;

uniqueness for b

b

proof end;

correctness ;

:: deftheorem SingleFunc defines singleton ROUGHS_5:def 2 :

for R being non empty set

for b_{2} being Function of R,(bool R) holds

( b_{2} = singleton R iff for x being Element of R holds b_{2} . x = {x} );

for R being non empty set

for b

( b

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))

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 :: ROUGHS_5:4

::: $f^d$

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 )

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 ;

ex b_{1} being Function of the carrier of R,(bool the carrier of R) st

for x being Element of R holds b_{1} . x = Coim ( the InternalRel of R,x)

for b_{1}, b_{2} being Function of the carrier of R,(bool the carrier of R) st ( for x being Element of R holds b_{1} . x = Coim ( the InternalRel of R,x) ) & ( for x being Element of R holds b_{2} . x = Coim ( the InternalRel of R,x) ) holds

b_{1} = b_{2}

;

end;
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 for x being Element of R holds it . x = Coim ( the InternalRel of R,x);

ex b

for x being Element of R holds b

proof end;

uniqueness for b

b

proof end;

correctness ;

:: deftheorem DefUnc defines UncertaintyMap ROUGHS_5:def 3 :

for R being non empty RelStr

for b_{2} being Function of the carrier of R,(bool the carrier of R) holds

( b_{2} = UncertaintyMap R iff for x being Element of R holds b_{2} . x = Coim ( the InternalRel of R,x) );

for R being non empty RelStr

for b

( b

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 )

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 ;

ex b_{1} being Function of the carrier of R,(bool the carrier of R) st

for u being Element of R holds b_{1} . u = Im ( the InternalRel of R,u)

for b_{1}, b_{2} being Function of the carrier of R,(bool the carrier of R) st ( for u being Element of R holds b_{1} . u = Im ( the InternalRel of R,u) ) & ( for u being Element of R holds b_{2} . u = Im ( the InternalRel of R,u) ) holds

b_{1} = b_{2}

end;
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 for u being Element of R holds it . u = Im ( the InternalRel of R,u);

ex b

for u being Element of R holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem DefTau defines tau ROUGHS_5:def 4 :

for R being non empty RelStr

for b_{2} being Function of the carrier of R,(bool the carrier of R) holds

( b_{2} = tau R iff for u being Element of R holds b_{2} . u = Im ( the InternalRel of R,u) );

for R being non empty RelStr

for b

( b

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) )

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 )

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

ex b_{1} being map of R st

for x being Subset of R holds b_{1} . x = { u where u is Element of R : f . u meets x }

for b_{1}, b_{2} being map of R st ( for x being Subset of R holds b_{1} . x = { u where u is Element of R : f . u meets x } ) & ( for x being Subset of R holds b_{2} . x = { u where u is Element of R : f . u meets x } ) holds

b_{1} = b_{2}

end;
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 for x being Subset of R holds it . x = { u where u is Element of R : f . u meets x } ;

ex b

for x being Subset of R holds b

proof end;

uniqueness for b

b

proof 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_{3} being map of R holds

( b_{3} = ff_0 f iff for x being Subset of R holds b_{3} . x = { u where u is Element of R : f . u meets x } );

for R being non empty RelStr

for f being Function of the carrier of R,(bool the carrier of R)

for b

( b

definition

let R be non empty RelStr ;

coherence

ff_0 (tau R) is map of R ;

coherence

ff_0 (UncertaintyMap R) is map of R ;

end;
coherence

ff_0 (tau R) is map of R ;

coherence

ff_0 (UncertaintyMap R) is map of R ;

:: deftheorem defines f_1 ROUGHS_5:def 7 :

for R being non empty RelStr holds f_1 R = ff_0 (UncertaintyMap R);

for R being non empty RelStr holds f_1 R = ff_0 (UncertaintyMap R);

theorem :: ROUGHS_5:11

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 )

( 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 :: 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

id (bool the carrier of R) cc= f_0 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

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) . {} = {}

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

ff_0 f is empty-preserving by Proph;

end;
let f be Function of the carrier of R,(bool the carrier of R);

coherence

ff_0 f is empty-preserving by Proph;

registration

let R be non empty reflexive RelStr ;

coherence

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

end;
coherence

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

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

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

(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

(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 )

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 )

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 )

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 }

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 }

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 }

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 )

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 )

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 )

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

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

for w being Element of R holds w in (tau R) . w

proof end;

registration

let R be non empty reflexive RelStr ;

coherence

UncertaintyMap R is map-reflexive by ReflUnc;

coherence

tau R is map-reflexive by ReflTau;

end;
coherence

UncertaintyMap R is map-reflexive by ReflUnc;

coherence

tau R is map-reflexive by ReflTau;

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) )

( (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

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 ;

coherence

f_0 R is c=-monotone by F0Mono;

coherence

f_1 R is c=-monotone by F1Mono;

end;
coherence

f_0 R is c=-monotone by F0Mono;

coherence

f_1 R is c=-monotone by F1Mono;

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)

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

theorem :: ROUGHS_5:44

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)

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

theorem :: ROUGHS_5:47

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)

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

theorem :: ROUGHS_5:50

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)

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

theorem :: ROUGHS_5:53