:: COH_SP semantic presentation

definition

let c₁ be set ;
canceled;
attr a₁ is binary_complete means :Def2: :: COH_SP:def 2
for b₁ being set st b₁ c= a₁ & ( for b₂, b₃ being set st b₂ in b₁ & b₃ in b₁ holds
b₂ \/ b₃ in a₁ ) holds
union b₁ in a₁;

end;

:: deftheorem Def1 COH_SP:def 1 :

:: deftheorem Def2 defines binary_complete COH_SP:def 2 :

registration

cluster non empty subset-closed binary_complete set ;
existence

proof end;

end;

definition

mode Coherence_Space is non empty subset-closed binary_complete set ;

end;

theorem Th1: :: COH_SP:1

for b₁ being Coherence_Space holds {} in b₁

proof end;

theorem Th2: :: COH_SP:2

for b₁ being set holds bool b₁ is Coherence_Space

proof end;

theorem Th3: :: COH_SP:3

{{} } is Coherence_Space by Th2, ZFMISC_1:1;

theorem Th4: :: COH_SP:4

for b₁ being set
for b₂ being Coherence_Space st b₁ in union b₂ holds
{b₁} in b₂

proof end;

definition

let c₁ be Coherence_Space;
func Web c₁ -> Tolerance of union a₁ means :Def3: :: COH_SP:def 3
for b₁, b₂ being set holds
( [b₁,b₂] in a₂ iff ex b₃ being set st
( b₃ in a₁ & b₁ in b₃ & b₂ in b₃ ) );
existence

proof end;

uniqueness by TOLER_1:52;

end;

:: deftheorem Def3 defines Web COH_SP:def 3 :

theorem Th5: :: COH_SP:5

for b₁ being Coherence_Space
for b₂ being Tolerance of union b₁ holds
( b₂ = Web b₁ iff for b₃, b₄ being set holds
( [b₃,b₄] in b₂ iff {b₃,b₄} in b₁ ) )

proof end;

theorem Th6: :: COH_SP:6

for b₁ being set
for b₂ being Coherence_Space holds
( b₁ in b₂ iff for b₃, b₄ being set st b₃ in b₁ & b₄ in b₁ holds
{b₃,b₄} in b₂ )

proof end;

theorem Th7: :: COH_SP:7

for b₁ being set
for b₂ being Coherence_Space holds
( b₁ in b₂ iff for b₃, b₄ being set st b₃ in b₁ & b₄ in b₁ holds
[b₃,b₄] in Web b₂ )

proof end;

theorem Th8: :: COH_SP:8

for b₁ being set
for b₂ being Coherence_Space st ( for b₃, b₄ being set st b₃ in b₁ & b₄ in b₁ holds
{b₃,b₄} in b₂ ) holds
b₁ c= union b₂

proof end;

theorem Th9: :: COH_SP:9

for b₁, b₂ being Coherence_Space st Web b₁ = Web b₂ holds
b₁ = b₂

proof end;

theorem Th10: :: COH_SP:10

for b₁ being Coherence_Space st union b₁ in b₁ holds
b₁ = bool (union b₁)

proof end;

theorem Th11: :: COH_SP:11

for b₁ being Coherence_Space st b₁ = bool (union b₁) holds
Web b₁ = Total (union b₁)

proof end;

definition

let c₁ be set ;
let c₂ be Tolerance of c₁;
func CohSp c₂ -> Coherence_Space means :Def4: :: COH_SP:def 4
for b₁ being set holds
( b₁ in a₃ iff for b₂, b₃ being set st b₂ in b₁ & b₃ in b₁ holds
[b₂,b₃] in a₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines CohSp COH_SP:def 4 :

theorem Th12: :: COH_SP:12

for b₁ being set
for b₂ being Tolerance of b₁ holds Web (CohSp b₂) = b₂

proof end;

theorem Th13: :: COH_SP:13

for b₁ being Coherence_Space holds CohSp (Web b₁) = b₁

proof end;

theorem Th14: :: COH_SP:14

for b₁, b₂ being set
for b₃ being Tolerance of b₁ holds
( b₂ in CohSp b₃ iff b₂ is TolSet of b₃ )

proof end;

theorem Th15: :: COH_SP:15

for b₁ being set
for b₂ being Tolerance of b₁ holds CohSp b₂ = TolSets b₂

proof end;

definition

let c₁ be set ;
func CSp c₁ -> set equals :: COH_SP:def 5
{ b₁ where B is Subset-Family of a₁ : b₁ is Coherence_Space } ;
coherence ;

end;

:: deftheorem Def5 defines CSp COH_SP:def 5 :

registration

let c₁ be set ;
cluster CSp a₁ -> non empty ;
coherence

proof end;

end;

registration

let c₁ be set ;
cluster -> non empty subset-closed binary_complete Element of CSp a₁;
coherence

proof end;

end;

theorem Th16: :: COH_SP:16

for b₁, b₂, b₃ being set
for b₄ being Element of CSp b₁ st {b₂,b₃} in b₄ holds
( b₂ in union b₄ & b₃ in union b₄ )

proof end;

definition

let c₁ be set ;
canceled;
func FuncsC c₁ -> set equals :: COH_SP:def 7
union { (Funcs (union b₁),(union b₂)) where B is Element of CSp a₁, B is Element of CSp a₁ : verum } ;
coherence ;

end;

:: deftheorem Def6 COH_SP:def 6 :

:: deftheorem Def7 defines FuncsC COH_SP:def 7 :

registration

let c₁ be set ;
cluster FuncsC a₁ -> non empty functional ;
coherence

proof end;

end;

theorem Th17: :: COH_SP:17

for b₁, b₂ being set holds
( b₁ in FuncsC b₂ iff ex b₃, b₄ being Element of CSp b₂ st
( ( union b₄ = {} implies union b₃ = {} ) & b₁ is Function of union b₃, union b₄ ) )

proof end;

definition

let c₁ be set ;
func MapsC c₁ -> set equals :: COH_SP:def 8
{ [[b₁,b₂],b₃] where B is Element of CSp a₁, B is Element of CSp a₁, B is Element of FuncsC a₁ : ( ( union b₂ = {} implies union b₁ = {} ) & b₃ is Function of union b₁, union b₂ & ( for b₁, b₂ being set st {b₄,b₅} in b₁ holds
{(b₃ . b₄),(b₃ . b₅)} in b₂ ) ) } ;
coherence ;

end;

:: deftheorem Def8 defines MapsC COH_SP:def 8 :

registration

let c₁ be set ;
cluster MapsC a₁ -> non empty ;
coherence

proof end;

end;

theorem Th18: :: COH_SP:18

for b₁ being set
for b₂ being Element of MapsC b₁ ex b₃ being Element of FuncsC b₁ex b₄, b₅ being Element of CSp b₁ st
( b₂ = [[b₄,b₅],b₃] & ( union b₅ = {} implies union b₄ = {} ) & b₃ is Function of union b₄, union b₅ & ( for b₆, b₇ being set st {b₆,b₇} in b₄ holds
{(b₃ . b₆),(b₃ . b₇)} in b₅ ) )

proof end;

theorem Th19: :: COH_SP:19

for b₁ being set
for b₂, b₃ being Element of CSp b₁
for b₄ being Function of union b₂, union b₃ st ( union b₃ = {} implies union b₂ = {} ) & ( for b₅, b₆ being set st {b₅,b₆} in b₂ holds
{(b₄ . b₅),(b₄ . b₆)} in b₃ ) holds
[[b₂,b₃],b₄] in MapsC b₁

proof end;

registration

let c₁ be set ;
let c₂ be Element of MapsC c₁;
cluster a₂ `2 -> Relation-like Function-like ;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be Element of MapsC c₁;
canceled;
func dom c₂ -> Element of CSp a₁ equals :: COH_SP:def 10
(a₂ `1 ) `1 ;
coherence

proof end;

func cod c₂ -> Element of CSp a₁ equals :: COH_SP:def 11
(a₂ `1 ) `2 ;
coherence

proof end;

end;

:: deftheorem Def9 COH_SP:def 9 :

:: deftheorem Def10 defines dom COH_SP:def 10 :

:: deftheorem Def11 defines cod COH_SP:def 11 :

theorem Th20: :: COH_SP:20

for b₁ being set
for b₂ being Element of MapsC b₁ holds b₂ = [[(dom b₂),(cod b₂)],(b₂ `2 )]

proof end;

Lemma15: for b₁ being set
for b₂, b₃ being Element of MapsC b₁ st b₂ `2 = b₃ `2 & dom b₂ = dom b₃ & cod b₂ = cod b₃ holds
b₂ = b₃

proof end;

definition

let c₁ be set ;
let c₂ be Element of CSp c₁;
func id$ c₂ -> Element of MapsC a₁ equals :: COH_SP:def 12
[[a₂,a₂],(id (union a₂))];
coherence

proof end;

end;

:: deftheorem Def12 defines id$ COH_SP:def 12 :

Lemma16: for b₁, b₂, b₃, b₄, b₅, b₆ being set st [[b₁,b₃],b₅] = [[b₂,b₄],b₆] holds
( b₁ = b₂ & b₃ = b₄ )

proof end;

theorem Th21: :: COH_SP:21

for b₁ being set
for b₂ being Element of MapsC b₁ holds
( ( union (cod b₂) <> {} or union (dom b₂) = {} ) & b₂ `2 is Function of union (dom b₂), union (cod b₂) & ( for b₃, b₄ being set st {b₃,b₄} in dom b₂ holds
{((b₂ `2 ) . b₃),((b₂ `2 ) . b₄)} in cod b₂ ) )

proof end;

definition

let c₁ be set ;
let c₂, c₃ be Element of MapsC c₁;
assume E18: cod c₂ = dom c₃ ;
func c₃ * c₂ -> Element of MapsC a₁ equals :Def13: :: COH_SP:def 13
[[(dom a₂),(cod a₃)],((a₃ `2 ) * (a₂ `2 ))];
coherence

proof end;

end;

:: deftheorem Def13 defines * COH_SP:def 13 :

theorem Th22: :: COH_SP:22

for b₁ being set
for b₂, b₃ being Element of MapsC b₁ st dom b₂ = cod b₃ holds
( (b₂ * b₃) `2 = (b₂ `2 ) * (b₃ `2 ) & dom (b₂ * b₃) = dom b₃ & cod (b₂ * b₃) = cod b₂ )

proof end;

theorem Th23: :: COH_SP:23

for b₁ being set
for b₂, b₃, b₄ being Element of MapsC b₁ st dom b₂ = cod b₃ & dom b₄ = cod b₂ holds
b₄ * (b₂ * b₃) = (b₄ * b₂) * b₃

proof end;

theorem Th24: :: COH_SP:24

for b₁ being set
for b₂ being Element of CSp b₁ holds
( (id$ b₂) `2 = id (union b₂) & dom (id$ b₂) = b₂ & cod (id$ b₂) = b₂ )

proof end;

theorem Th25: :: COH_SP:25

for b₁ being set
for b₂ being Element of MapsC b₁ holds
( b₂ * (id$ (dom b₂)) = b₂ & (id$ (cod b₂)) * b₂ = b₂ )

proof end;

definition

let c₁ be set ;
func CDom c₁ -> Function of MapsC a₁, CSp a₁ means :Def14: :: COH_SP:def 14
for b₁ being Element of MapsC a₁ holds a₂ . b₁ = dom b₁;
existence

proof end;

uniqueness

proof end;

func CCod c₁ -> Function of MapsC a₁, CSp a₁ means :Def15: :: COH_SP:def 15
for b₁ being Element of MapsC a₁ holds a₂ . b₁ = cod b₁;
existence

proof end;

uniqueness

proof end;

func CComp c₁ -> PartFunc of [:(MapsC a₁),(MapsC a₁):], MapsC a₁ means :Def16: :: COH_SP:def 16
( ( for b₁, b₂ being Element of MapsC a₁ holds
( [b₁,b₂] in dom a₂ iff dom b₁ = cod b₂ ) ) & ( for b₁, b₂ being Element of MapsC a₁ st dom b₁ = cod b₂ holds
a₂ . [b₁,b₂] = b₁ * b₂ ) );
existence

proof end;

uniqueness

proof end;

func CId c₁ -> Function of CSp a₁, MapsC a₁ means :Def17: :: COH_SP:def 17
for b₁ being Element of CSp a₁ holds a₂ . b₁ = id$ b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines CDom COH_SP:def 14 :

:: deftheorem Def15 defines CCod COH_SP:def 15 :

:: deftheorem Def16 defines CComp COH_SP:def 16 :

:: deftheorem Def17 defines CId COH_SP:def 17 :

theorem Th26: :: COH_SP:26

for b₁ being set holds CatStr(# (CSp b₁),(MapsC b₁),(CDom b₁),(CCod b₁),(CComp b₁),(CId b₁) #) is Category

proof end;

definition

let c₁ be set ;
func CohCat c₁ -> Category equals :: COH_SP:def 18
CatStr(# (CSp a₁),(MapsC a₁),(CDom a₁),(CCod a₁),(CComp a₁),(CId a₁) #);
coherence by Th26;

end;

:: deftheorem Def18 defines CohCat COH_SP:def 18 :

definition

let c₁ be set ;
func Toler c₁ -> set means :Def19: :: COH_SP:def 19
for b₁ being set holds
( b₁ in a₂ iff b₁ is Tolerance of a₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def19 defines Toler COH_SP:def 19 :

registration

let c₁ be set ;
cluster Toler a₁ -> non empty ;
coherence

proof end;

end;

definition

let c₁ be set ;
func Toler_on_subsets c₁ -> set equals :: COH_SP:def 20
union { (Toler b₁) where B is Subset of a₁ : verum } ;
coherence ;

end;

:: deftheorem Def20 defines Toler_on_subsets COH_SP:def 20 :

registration

let c₁ be set ;
cluster Toler_on_subsets a₁ -> non empty ;
coherence

proof end;

end;

theorem Th27: :: COH_SP:27

for b₁, b₂ being set holds
( b₁ in Toler_on_subsets b₂ iff ex b₃ being set st
( b₃ c= b₂ & b₁ is Tolerance of b₃ ) )

proof end;

theorem Th28: :: COH_SP:28

for b₁ being set holds Total b₁ in Toler b₁ by Def19;

theorem Th29: :: COH_SP:29

canceled;

theorem Th30: :: COH_SP:30

for b₁ being set holds {} in Toler_on_subsets b₁

proof end;

theorem Th31: :: COH_SP:31

for b₁, b₂ being set st b₁ c= b₂ holds
Total b₁ in Toler_on_subsets b₂

proof end;

theorem Th32: :: COH_SP:32

for b₁, b₂ being set st b₁ c= b₂ holds
id b₁ in Toler_on_subsets b₂

proof end;

theorem Th33: :: COH_SP:33

for b₁ being set holds Total b₁ in Toler_on_subsets b₁ by Th31;

theorem Th34: :: COH_SP:34

for b₁ being set holds id b₁ in Toler_on_subsets b₁ by Th32;

definition

let c₁ be set ;
func TOL c₁ -> set equals :: COH_SP:def 21
{ [b₁,b₂] where B is Element of Toler_on_subsets a₁, B is Subset of a₁ : b₁ is Tolerance of b₂ } ;
coherence ;

end;

:: deftheorem Def21 defines TOL COH_SP:def 21 :

registration

let c₁ be set ;
cluster TOL a₁ -> non empty ;
coherence

proof end;

end;

theorem Th35: :: COH_SP:35

for b₁ being set holds [{} ,{} ] in TOL b₁

proof end;

theorem Th36: :: COH_SP:36

for b₁, b₂ being set st b₁ c= b₂ holds
[(id b₁),b₁] in TOL b₂

proof end;

theorem Th37: :: COH_SP:37

for b₁, b₂ being set st b₁ c= b₂ holds
[(Total b₁),b₁] in TOL b₂

proof end;

theorem Th38: :: COH_SP:38

for b₁ being set holds [(id b₁),b₁] in TOL b₁ by Th36;

theorem Th39: :: COH_SP:39

for b₁ being set holds [(Total b₁),b₁] in TOL b₁ by Th37;

definition

let c₁ be set ;
let c₂ be Element of TOL c₁;
redefine func `2 as c₂ `2 -> Subset of a₁;
coherence

proof end;

redefine func `1 as c₂ `1 -> Tolerance of a₂ `2 ;
coherence

proof end;

end;

definition

let c₁ be set ;
func FuncsT c₁ -> set equals :: COH_SP:def 22
union { (Funcs (b₁ `2 ),(b₂ `2 )) where B is Element of TOL a₁, B is Element of TOL a₁ : verum } ;
coherence ;

end;

:: deftheorem Def22 defines FuncsT COH_SP:def 22 :

registration

let c₁ be set ;
cluster FuncsT a₁ -> non empty functional ;
coherence

proof end;

end;

theorem Th40: :: COH_SP:40

for b₁, b₂ being set holds
( b₁ in FuncsT b₂ iff ex b₃, b₄ being Element of TOL b₂ st
( ( b₄ `2 = {} implies b₃ `2 = {} ) & b₁ is Function of b₃ `2 ,b₄ `2 ) )

proof end;

definition

let c₁ be set ;
func MapsT c₁ -> set equals :: COH_SP:def 23
{ [[b₁,b₂],b₃] where B is Element of TOL a₁, B is Element of TOL a₁, B is Element of FuncsT a₁ : ( ( b₂ `2 = {} implies b₁ `2 = {} ) & b₃ is Function of b₁ `2 ,b₂ `2 & ( for b₁, b₂ being set st [b₄,b₅] in b₁ `1 holds
[(b₃ . b₄),(b₃ . b₅)] in b₂ `1 ) ) } ;
coherence ;

end;

:: deftheorem Def23 defines MapsT COH_SP:def 23 :

registration

let c₁ be set ;
cluster MapsT a₁ -> non empty ;
coherence

proof end;

end;

theorem Th41: :: COH_SP:41

for b₁ being set
for b₂ being Element of MapsT b₁ ex b₃ being Element of FuncsT b₁ex b₄, b₅ being Element of TOL b₁ st
( b₂ = [[b₄,b₅],b₃] & ( b₅ `2 = {} implies b₄ `2 = {} ) & b₃ is Function of b₄ `2 ,b₅ `2 & ( for b₆, b₇ being set st [b₆,b₇] in b₄ `1 holds
[(b₃ . b₆),(b₃ . b₇)] in b₅ `1 ) )

proof end;

theorem Th42: :: COH_SP:42

for b₁ being set
for b₂, b₃ being Element of TOL b₁
for b₄ being Function of b₂ `2 ,b₃ `2 st ( b₃ `2 = {} implies b₂ `2 = {} ) & ( for b₅, b₆ being set st [b₅,b₆] in b₂ `1 holds
[(b₄ . b₅),(b₄ . b₆)] in b₃ `1 ) holds
[[b₂,b₃],b₄] in MapsT b₁

proof end;

registration

let c₁ be set ;
let c₂ be Element of MapsT c₁;
cluster a₂ `2 -> Relation-like Function-like ;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be Element of MapsT c₁;
canceled;
func dom c₂ -> Element of TOL a₁ equals :: COH_SP:def 25
(a₂ `1 ) `1 ;
coherence

proof end;

func cod c₂ -> Element of TOL a₁ equals :: COH_SP:def 26
(a₂ `1 ) `2 ;
coherence

proof end;

end;

:: deftheorem Def24 COH_SP:def 24 :

:: deftheorem Def25 defines dom COH_SP:def 25 :

:: deftheorem Def26 defines cod COH_SP:def 26 :

theorem Th43: :: COH_SP:43

for b₁ being set
for b₂ being Element of MapsT b₁ holds b₂ = [[(dom b₂),(cod b₂)],(b₂ `2 )]

proof end;

Lemma38: for b₁ being set
for b₂, b₃ being Element of MapsT b₁ st b₂ `2 = b₃ `2 & dom b₂ = dom b₃ & cod b₂ = cod b₃ holds
b₂ = b₃

proof end;

definition

let c₁ be set ;
let c₂ be Element of TOL c₁;
func id$ c₂ -> Element of MapsT a₁ equals :: COH_SP:def 27
[[a₂,a₂],(id (a₂ `2 ))];
coherence

proof end;

end;

:: deftheorem Def27 defines id$ COH_SP:def 27 :

theorem Th44: :: COH_SP:44

for b₁ being set
for b₂ being Element of MapsT b₁ holds
( ( (cod b₂) `2 <> {} or (dom b₂) `2 = {} ) & b₂ `2 is Function of (dom b₂) `2 ,(cod b₂) `2 & ( for b₃, b₄ being set st [b₃,b₄] in (dom b₂) `1 holds
[((b₂ `2 ) . b₃),((b₂ `2 ) . b₄)] in (cod b₂) `1 ) )

proof end;

definition

let c₁ be set ;
let c₂, c₃ be Element of MapsT c₁;
assume E40: cod c₂ = dom c₃ ;
func c₃ * c₂ -> Element of MapsT a₁ equals :Def28: :: COH_SP:def 28
[[(dom a₂),(cod a₃)],((a₃ `2 ) * (a₂ `2 ))];
coherence

proof end;

end;

:: deftheorem Def28 defines * COH_SP:def 28 :

theorem Th45: :: COH_SP:45

for b₁ being set
for b₂, b₃ being Element of MapsT b₁ st dom b₂ = cod b₃ holds
( (b₂ * b₃) `2 = (b₂ `2 ) * (b₃ `2 ) & dom (b₂ * b₃) = dom b₃ & cod (b₂ * b₃) = cod b₂ )

proof end;

theorem Th46: :: COH_SP:46

for b₁ being set
for b₂, b₃, b₄ being Element of MapsT b₁ st dom b₂ = cod b₃ & dom b₄ = cod b₂ holds
b₄ * (b₂ * b₃) = (b₄ * b₂) * b₃

proof end;

theorem Th47: :: COH_SP:47

for b₁ being set
for b₂ being Element of TOL b₁ holds
( (id$ b₂) `2 = id (b₂ `2 ) & dom (id$ b₂) = b₂ & cod (id$ b₂) = b₂ )

proof end;

theorem Th48: :: COH_SP:48

for b₁ being set
for b₂ being Element of MapsT b₁ holds
( b₂ * (id$ (dom b₂)) = b₂ & (id$ (cod b₂)) * b₂ = b₂ )

proof end;

definition

let c₁ be set ;
func fDom c₁ -> Function of MapsT a₁, TOL a₁ means :Def29: :: COH_SP:def 29
for b₁ being Element of MapsT a₁ holds a₂ . b₁ = dom b₁;
existence

proof end;

uniqueness

proof end;

func fCod c₁ -> Function of MapsT a₁, TOL a₁ means :Def30: :: COH_SP:def 30
for b₁ being Element of MapsT a₁ holds a₂ . b₁ = cod b₁;
existence

proof end;

uniqueness

proof end;

func fComp c₁ -> PartFunc of [:(MapsT a₁),(MapsT a₁):], MapsT a₁ means :Def31: :: COH_SP:def 31
( ( for b₁, b₂ being Element of MapsT a₁ holds
( [b₁,b₂] in dom a₂ iff dom b₁ = cod b₂ ) ) & ( for b₁, b₂ being Element of MapsT a₁ st dom b₁ = cod b₂ holds
a₂ . [b₁,b₂] = b₁ * b₂ ) );
existence

proof end;

uniqueness

proof end;

func fId c₁ -> Function of TOL a₁, MapsT a₁ means :Def32: :: COH_SP:def 32
for b₁ being Element of TOL a₁ holds a₂ . b₁ = id$ b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def29 defines fDom COH_SP:def 29 :

:: deftheorem Def30 defines fCod COH_SP:def 30 :

:: deftheorem Def31 defines fComp COH_SP:def 31 :

:: deftheorem Def32 defines fId COH_SP:def 32 :

theorem Th49: :: COH_SP:49

for b₁ being set holds CatStr(# (TOL b₁),(MapsT b₁),(fDom b₁),(fCod b₁),(fComp b₁),(fId b₁) #) is Category

proof end;

definition

let c₁ be set ;
func TolCat c₁ -> Category equals :: COH_SP:def 33
CatStr(# (TOL a₁),(MapsT a₁),(fDom a₁),(fCod a₁),(fComp a₁),(fId a₁) #);
coherence by Th49;

end;

:: deftheorem Def33 defines TolCat COH_SP:def 33 :