:: by Zbigniew Karno and Toshihiko Watanabe

::

:: Received July 16, 1992

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

theorem Th1: :: TDLAT_2:1

for T being TopSpace

for A being Subset of T holds

( Int (Cl (Int A)) c= Int (Cl A) & Int (Cl (Int A)) c= Cl (Int A) )

for A being Subset of T holds

( Int (Cl (Int A)) c= Int (Cl A) & Int (Cl (Int A)) c= Cl (Int A) )

proof end;

theorem Th2: :: TDLAT_2:2

for T being TopSpace

for A being Subset of T holds

( Cl (Int A) c= Cl (Int (Cl A)) & Int (Cl A) c= Cl (Int (Cl A)) )

for A being Subset of T holds

( Cl (Int A) c= Cl (Int (Cl A)) & Int (Cl A) c= Cl (Int (Cl A)) )

proof end;

theorem Th5: :: TDLAT_2:5

for T being TopSpace

for A being Subset of T st A c= Cl (Int A) holds

A \/ (Int (Cl A)) c= Cl (Int (A \/ (Int (Cl A))))

for A being Subset of T st A c= Cl (Int A) holds

A \/ (Int (Cl A)) c= Cl (Int (A \/ (Int (Cl A))))

proof end;

theorem Th6: :: TDLAT_2:6

for T being TopSpace

for A being Subset of T st Int (Cl A) c= A holds

Int (Cl (A /\ (Cl (Int A)))) c= A /\ (Cl (Int A))

for A being Subset of T st Int (Cl A) c= A holds

Int (Cl (A /\ (Cl (Int A)))) c= A /\ (Cl (Int A))

proof end;

::Properties of the Closure Operation Cl (see also PCOMPS_1).

theorem Th7: :: TDLAT_2:7

for T being TopSpace

for F being Subset-Family of T holds Cl F = { A where A is Subset of T : ex B being Subset of T st

( A = Cl B & B in F ) }

for F being Subset-Family of T holds Cl F = { A where A is Subset of T : ex B being Subset of T st

( A = Cl B & B in F ) }

proof end;

theorem :: TDLAT_2:12

for T being TopSpace

for F being Subset-Family of T

for A being Subset of T st A in F holds

( meet (Cl F) c= Cl A & Cl A c= union (Cl F) )

for F being Subset-Family of T

for A being Subset of T st A in F holds

( meet (Cl F) c= Cl A & Cl A c= union (Cl F) )

proof end;

::for F being Subset-Family of T holds union F c= union(Cl F);

::(see PCOMPS_1:22)

::(see PCOMPS_1:22)

definition

let T be TopSpace;

let F be Subset-Family of T;

ex b_{1} being Subset-Family of T st

for A being Subset of T holds

( A in b_{1} iff ex B being Subset of T st

( A = Int B & B in F ) )

for b_{1}, b_{2} being Subset-Family of T st ( for A being Subset of T holds

( A in b_{1} iff ex B being Subset of T st

( A = Int B & B in F ) ) ) & ( for A being Subset of T holds

( A in b_{2} iff ex B being Subset of T st

( A = Int B & B in F ) ) ) holds

b_{1} = b_{2}

for b_{1}, b_{2} being Subset-Family of T st ( for A being Subset of T holds

( A in b_{1} iff ex B being Subset of T st

( A = Int B & B in b_{2} ) ) ) holds

for A being Subset of T holds

( A in b_{1} iff ex B being Subset of T st

( A = Int B & B in b_{1} ) )

end;
let F be Subset-Family of T;

func Int F -> Subset-Family of T means :Def1: :: TDLAT_2:def 1

for A being Subset of T holds

( A in it iff ex B being Subset of T st

( A = Int B & B in F ) );

existence for A being Subset of T holds

( A in it iff ex B being Subset of T st

( A = Int B & B in F ) );

ex b

for A being Subset of T holds

( A in b

( A = Int B & B in F ) )

proof end;

uniqueness for b

( A in b

( A = Int B & B in F ) ) ) & ( for A being Subset of T holds

( A in b

( A = Int B & B in F ) ) ) holds

b

proof end;

projectivity for b

( A in b

( A = Int B & B in b

for A being Subset of T holds

( A in b

( A = Int B & B in b

proof end;

:: deftheorem Def1 defines Int TDLAT_2:def 1 :

for T being TopSpace

for F, b_{3} being Subset-Family of T holds

( b_{3} = Int F iff for A being Subset of T holds

( A in b_{3} iff ex B being Subset of T st

( A = Int B & B in F ) ) );

for T being TopSpace

for F, b

( b

( A in b

( A = Int B & B in F ) ) );

::Properties of the Interior Operation Int.

theorem Th16: :: TDLAT_2:16

for T being TopSpace

for F being Subset-Family of T holds Int F = { A where A is Subset of T : ex B being Subset of T st

( A = Int B & B in F ) }

for F being Subset-Family of T holds Int F = { A where A is Subset of T : ex B being Subset of T st

( A = Int B & B in F ) }

proof end;

::$CT

theorem Th19: :: TDLAT_2:20

for T being TopSpace

for A being Subset of T

for F being Subset-Family of T st F = {A} holds

Int F = {(Int A)}

for A being Subset of T

for F being Subset-Family of T st F = {A} holds

Int F = {(Int A)}

proof end;

theorem :: TDLAT_2:25

for T being TopSpace

for F being Subset-Family of T

for A being Subset of T st A in F holds

( Int A c= union (Int F) & meet (Int F) c= Int A )

for F being Subset-Family of T

for A being Subset of T st A in F holds

( Int A c= union (Int F) & meet (Int F) c= Int A )

proof end;

theorem :: TDLAT_2:30

for T being TopSpace

for F being Subset-Family of T st F is finite holds

Int (meet F) = meet (Int F)

for F being Subset-Family of T st F is finite holds

Int (meet F) = meet (Int F)

proof end;

theorem Th30: :: TDLAT_2:31

for T being non empty TopSpace

for F being Subset-Family of T holds Cl (Int F) = { A where A is Subset of T : ex B being Subset of T st

( A = Cl (Int B) & B in F ) }

for F being Subset-Family of T holds Cl (Int F) = { A where A is Subset of T : ex B being Subset of T st

( A = Cl (Int B) & B in F ) }

proof end;

theorem Th31: :: TDLAT_2:32

for T being non empty TopSpace

for F being Subset-Family of T holds Int (Cl F) = { A where A is Subset of T : ex B being Subset of T st

( A = Int (Cl B) & B in F ) }

for F being Subset-Family of T holds Int (Cl F) = { A where A is Subset of T : ex B being Subset of T st

( A = Int (Cl B) & B in F ) }

proof end;

theorem Th32: :: TDLAT_2:33

for T being non empty TopSpace

for F being Subset-Family of T holds Cl (Int (Cl F)) = { A where A is Subset of T : ex B being Subset of T st

( A = Cl (Int (Cl B)) & B in F ) }

for F being Subset-Family of T holds Cl (Int (Cl F)) = { A where A is Subset of T : ex B being Subset of T st

( A = Cl (Int (Cl B)) & B in F ) }

proof end;

theorem Th33: :: TDLAT_2:34

for T being non empty TopSpace

for F being Subset-Family of T holds Int (Cl (Int F)) = { A where A is Subset of T : ex B being Subset of T st

( A = Int (Cl (Int B)) & B in F ) }

for F being Subset-Family of T holds Int (Cl (Int F)) = { A where A is Subset of T : ex B being Subset of T st

( A = Int (Cl (Int B)) & B in F ) }

proof end;

theorem :: TDLAT_2:35

for T being non empty TopSpace

for F being Subset-Family of T holds Cl (Int (Cl (Int F))) = Cl (Int F)

for F being Subset-Family of T holds Cl (Int (Cl (Int F))) = Cl (Int F)

proof end;

theorem :: TDLAT_2:36

for T being non empty TopSpace

for F being Subset-Family of T holds Int (Cl (Int (Cl F))) = Int (Cl F)

for F being Subset-Family of T holds Int (Cl (Int (Cl F))) = Int (Cl F)

proof end;

theorem :: TDLAT_2:37

for T being non empty TopSpace

for F being Subset-Family of T holds union (Int (Cl F)) c= union (Cl (Int (Cl F)))

for F being Subset-Family of T holds union (Int (Cl F)) c= union (Cl (Int (Cl F)))

proof end;

theorem :: TDLAT_2:38

for T being non empty TopSpace

for F being Subset-Family of T holds meet (Int (Cl F)) c= meet (Cl (Int (Cl F)))

for F being Subset-Family of T holds meet (Int (Cl F)) c= meet (Cl (Int (Cl F)))

proof end;

theorem :: TDLAT_2:39

for T being non empty TopSpace

for F being Subset-Family of T holds union (Cl (Int F)) c= union (Cl (Int (Cl F)))

for F being Subset-Family of T holds union (Cl (Int F)) c= union (Cl (Int (Cl F)))

proof end;

theorem :: TDLAT_2:40

for T being non empty TopSpace

for F being Subset-Family of T holds meet (Cl (Int F)) c= meet (Cl (Int (Cl F)))

for F being Subset-Family of T holds meet (Cl (Int F)) c= meet (Cl (Int (Cl F)))

proof end;

theorem :: TDLAT_2:41

for T being non empty TopSpace

for F being Subset-Family of T holds union (Int (Cl (Int F))) c= union (Int (Cl F))

for F being Subset-Family of T holds union (Int (Cl (Int F))) c= union (Int (Cl F))

proof end;

theorem :: TDLAT_2:42

for T being non empty TopSpace

for F being Subset-Family of T holds meet (Int (Cl (Int F))) c= meet (Int (Cl F))

for F being Subset-Family of T holds meet (Int (Cl (Int F))) c= meet (Int (Cl F))

proof end;

theorem :: TDLAT_2:43

for T being non empty TopSpace

for F being Subset-Family of T holds union (Int (Cl (Int F))) c= union (Cl (Int F))

for F being Subset-Family of T holds union (Int (Cl (Int F))) c= union (Cl (Int F))

proof end;

theorem :: TDLAT_2:44

for T being non empty TopSpace

for F being Subset-Family of T holds meet (Int (Cl (Int F))) c= meet (Cl (Int F))

for F being Subset-Family of T holds meet (Int (Cl (Int F))) c= meet (Cl (Int F))

proof end;

theorem :: TDLAT_2:45

for T being non empty TopSpace

for F being Subset-Family of T holds union (Cl (Int (Cl F))) c= union (Cl F)

for F being Subset-Family of T holds union (Cl (Int (Cl F))) c= union (Cl F)

proof end;

theorem :: TDLAT_2:46

for T being non empty TopSpace

for F being Subset-Family of T holds meet (Cl (Int (Cl F))) c= meet (Cl F)

for F being Subset-Family of T holds meet (Cl (Int (Cl F))) c= meet (Cl F)

proof end;

theorem :: TDLAT_2:47

for T being non empty TopSpace

for F being Subset-Family of T holds union (Int F) c= union (Int (Cl (Int F)))

for F being Subset-Family of T holds union (Int F) c= union (Int (Cl (Int F)))

proof end;

theorem :: TDLAT_2:48

for T being non empty TopSpace

for F being Subset-Family of T holds meet (Int F) c= meet (Int (Cl (Int F)))

for F being Subset-Family of T holds meet (Int F) c= meet (Int (Cl (Int F)))

proof end;

theorem Th48: :: TDLAT_2:49

for T being non empty TopSpace

for F being Subset-Family of T holds union (Cl (Int F)) c= Cl (Int (union F))

for F being Subset-Family of T holds union (Cl (Int F)) c= Cl (Int (union F))

proof end;

theorem Th49: :: TDLAT_2:50

for T being non empty TopSpace

for F being Subset-Family of T holds Cl (Int (meet F)) c= meet (Cl (Int F))

for F being Subset-Family of T holds Cl (Int (meet F)) c= meet (Cl (Int F))

proof end;

theorem Th50: :: TDLAT_2:51

for T being non empty TopSpace

for F being Subset-Family of T holds union (Int (Cl F)) c= Int (Cl (union F))

for F being Subset-Family of T holds union (Int (Cl F)) c= Int (Cl (union F))

proof end;

theorem Th51: :: TDLAT_2:52

for T being non empty TopSpace

for F being Subset-Family of T holds Int (Cl (meet F)) c= meet (Int (Cl F))

for F being Subset-Family of T holds Int (Cl (meet F)) c= meet (Int (Cl F))

proof end;

theorem :: TDLAT_2:53

for T being non empty TopSpace

for F being Subset-Family of T holds union (Cl (Int (Cl F))) c= Cl (Int (Cl (union F)))

for F being Subset-Family of T holds union (Cl (Int (Cl F))) c= Cl (Int (Cl (union F)))

proof end;

theorem :: TDLAT_2:54

for T being non empty TopSpace

for F being Subset-Family of T holds Cl (Int (Cl (meet F))) c= meet (Cl (Int (Cl F)))

for F being Subset-Family of T holds Cl (Int (Cl (meet F))) c= meet (Cl (Int (Cl F)))

proof end;

theorem :: TDLAT_2:55

for T being non empty TopSpace

for F being Subset-Family of T holds union (Int (Cl (Int F))) c= Int (Cl (Int (union F)))

for F being Subset-Family of T holds union (Int (Cl (Int F))) c= Int (Cl (Int (union F)))

proof end;

theorem :: TDLAT_2:56

for T being non empty TopSpace

for F being Subset-Family of T holds Int (Cl (Int (meet F))) c= meet (Int (Cl (Int F)))

for F being Subset-Family of T holds Int (Cl (Int (meet F))) c= meet (Int (Cl (Int F)))

proof end;

theorem Th56: :: TDLAT_2:57

for T being non empty TopSpace

for F being Subset-Family of T st ( for A being Subset of T st A in F holds

A c= Cl (Int A) ) holds

( union F c= Cl (Int (union F)) & Cl (union F) = Cl (Int (Cl (union F))) )

for F being Subset-Family of T st ( for A being Subset of T st A in F holds

A c= Cl (Int A) ) holds

( union F c= Cl (Int (union F)) & Cl (union F) = Cl (Int (Cl (union F))) )

proof end;

theorem Th57: :: TDLAT_2:58

for T being non empty TopSpace

for F being Subset-Family of T st ( for A being Subset of T st A in F holds

Int (Cl A) c= A ) holds

( Int (Cl (meet F)) c= meet F & Int (Cl (Int (meet F))) = Int (meet F) )

for F being Subset-Family of T st ( for A being Subset of T st A in F holds

Int (Cl A) c= A ) holds

( Int (Cl (meet F)) c= meet F & Int (Cl (Int (meet F))) = Int (meet F) )

proof end;

theorem Th58: :: TDLAT_2:59

for T being non empty TopSpace

for A, B being Subset of T st B is condensed holds

( (Int (Cl (A \/ B))) \/ (A \/ B) = B iff A c= B )

for A, B being Subset of T st B is condensed holds

( (Int (Cl (A \/ B))) \/ (A \/ B) = B iff A c= B )

proof end;

theorem :: TDLAT_2:60

for T being non empty TopSpace

for A, B being Subset of T st A is condensed holds

( (Cl (Int (A /\ B))) /\ (A /\ B) = A iff A c= B )

for A, B being Subset of T st A is condensed holds

( (Cl (Int (A /\ B))) /\ (A /\ B) = A iff A c= B )

proof end;

theorem :: TDLAT_2:61

for T being non empty TopSpace

for A, B being Subset of T st A is closed_condensed & B is closed_condensed holds

( Int A c= Int B iff A c= B )

for A, B being Subset of T st A is closed_condensed & B is closed_condensed holds

( Int A c= Int B iff A c= B )

proof end;

theorem :: TDLAT_2:62

for T being non empty TopSpace

for A, B being Subset of T st A is open_condensed & B is open_condensed holds

( Cl A c= Cl B iff A c= B )

for A, B being Subset of T st A is open_condensed & B is open_condensed holds

( Cl A c= Cl B iff A c= B )

proof end;

theorem :: TDLAT_2:63

for T being non empty TopSpace

for A, B being Subset of T st A is closed_condensed & A c= B holds

Cl (Int (A /\ B)) = A

for A, B being Subset of T st A is closed_condensed & A c= B holds

Cl (Int (A /\ B)) = A

proof end;

theorem Th63: :: TDLAT_2:64

for T being non empty TopSpace

for A, B being Subset of T st B is open_condensed & A c= B holds

Int (Cl (A \/ B)) = B

for A, B being Subset of T st B is open_condensed & A c= B holds

Int (Cl (A \/ B)) = B

proof end;

definition

let T be non empty TopSpace;

let IT be Subset-Family of T;

end;
let IT be Subset-Family of T;

attr IT is domains-family means :: TDLAT_2:def 2

for A being Subset of T st A in IT holds

A is condensed ;

for A being Subset of T st A in IT holds

A is condensed ;

:: deftheorem defines domains-family TDLAT_2:def 2 :

for T being non empty TopSpace

for IT being Subset-Family of T holds

( IT is domains-family iff for A being Subset of T st A in IT holds

A is condensed );

for T being non empty TopSpace

for IT being Subset-Family of T holds

( IT is domains-family iff for A being Subset of T st A in IT holds

A is condensed );

theorem Th64: :: TDLAT_2:65

for T being non empty TopSpace

for F being Subset-Family of T holds

( F c= Domains_of T iff F is domains-family )

for F being Subset-Family of T holds

( F c= Domains_of T iff F is domains-family )

proof end;

theorem Th65: :: TDLAT_2:66

for T being non empty TopSpace

for F being Subset-Family of T st F is domains-family holds

( union F c= Cl (Int (union F)) & Cl (union F) = Cl (Int (Cl (union F))) )

for F being Subset-Family of T st F is domains-family holds

( union F c= Cl (Int (union F)) & Cl (union F) = Cl (Int (Cl (union F))) )

proof end;

theorem Th66: :: TDLAT_2:67

for T being non empty TopSpace

for F being Subset-Family of T st F is domains-family holds

( Int (Cl (meet F)) c= meet F & Int (Cl (Int (meet F))) = Int (meet F) )

for F being Subset-Family of T st F is domains-family holds

( Int (Cl (meet F)) c= meet F & Int (Cl (Int (meet F))) = Int (meet F) )

proof end;

theorem Th67: :: TDLAT_2:68

for T being non empty TopSpace

for F being Subset-Family of T st F is domains-family holds

(union F) \/ (Int (Cl (union F))) is condensed

for F being Subset-Family of T st F is domains-family holds

(union F) \/ (Int (Cl (union F))) is condensed

proof end;

theorem Th68: :: TDLAT_2:69

for T being non empty TopSpace

for F being Subset-Family of T holds

( ( for B being Subset of T st B in F holds

B c= (union F) \/ (Int (Cl (union F))) ) & ( for A being Subset of T st A is condensed & ( for B being Subset of T st B in F holds

B c= A ) holds

(union F) \/ (Int (Cl (union F))) c= A ) )

for F being Subset-Family of T holds

( ( for B being Subset of T st B in F holds

B c= (union F) \/ (Int (Cl (union F))) ) & ( for A being Subset of T st A is condensed & ( for B being Subset of T st B in F holds

B c= A ) holds

(union F) \/ (Int (Cl (union F))) c= A ) )

proof end;

theorem Th69: :: TDLAT_2:70

for T being non empty TopSpace

for F being Subset-Family of T st F is domains-family holds

(meet F) /\ (Cl (Int (meet F))) is condensed

for F being Subset-Family of T st F is domains-family holds

(meet F) /\ (Cl (Int (meet F))) is condensed

proof end;

theorem Th70: :: TDLAT_2:71

for T being non empty TopSpace

for F being Subset-Family of T holds

( ( for B being Subset of T st B in F holds

(meet F) /\ (Cl (Int (meet F))) c= B ) & ( F = {} or for A being Subset of T st A is condensed & ( for B being Subset of T st B in F holds

A c= B ) holds

A c= (meet F) /\ (Cl (Int (meet F))) ) )

for F being Subset-Family of T holds

( ( for B being Subset of T st B in F holds

(meet F) /\ (Cl (Int (meet F))) c= B ) & ( F = {} or for A being Subset of T st A is condensed & ( for B being Subset of T st B in F holds

A c= B ) holds

A c= (meet F) /\ (Cl (Int (meet F))) ) )

proof end;

definition

let T be non empty TopSpace;

let IT be Subset-Family of T;

end;
let IT be Subset-Family of T;

attr IT is closed-domains-family means :: TDLAT_2:def 3

for A being Subset of T st A in IT holds

A is closed_condensed ;

for A being Subset of T st A in IT holds

A is closed_condensed ;

:: deftheorem defines closed-domains-family TDLAT_2:def 3 :

for T being non empty TopSpace

for IT being Subset-Family of T holds

( IT is closed-domains-family iff for A being Subset of T st A in IT holds

A is closed_condensed );

for T being non empty TopSpace

for IT being Subset-Family of T holds

( IT is closed-domains-family iff for A being Subset of T st A in IT holds

A is closed_condensed );

theorem Th71: :: TDLAT_2:72

for T being non empty TopSpace

for F being Subset-Family of T holds

( F c= Closed_Domains_of T iff F is closed-domains-family )

for F being Subset-Family of T holds

( F c= Closed_Domains_of T iff F is closed-domains-family )

proof end;

theorem Th72: :: TDLAT_2:73

for T being non empty TopSpace

for F being Subset-Family of T st F is closed-domains-family holds

F is domains-family

for F being Subset-Family of T st F is closed-domains-family holds

F is domains-family

proof end;

theorem Th73: :: TDLAT_2:74

for T being non empty TopSpace

for F being Subset-Family of T st F is closed-domains-family holds

F is closed

for F being Subset-Family of T st F is closed-domains-family holds

F is closed

proof end;

theorem :: TDLAT_2:75

for T being non empty TopSpace

for F being Subset-Family of T st F is domains-family holds

Cl F is closed-domains-family

for F being Subset-Family of T st F is domains-family holds

Cl F is closed-domains-family

proof end;

theorem Th75: :: TDLAT_2:76

for T being non empty TopSpace

for F being Subset-Family of T st F is closed-domains-family holds

( Cl (union F) is closed_condensed & Cl (Int (meet F)) is closed_condensed )

for F being Subset-Family of T st F is closed-domains-family holds

( Cl (union F) is closed_condensed & Cl (Int (meet F)) is closed_condensed )

proof end;

theorem Th76: :: TDLAT_2:77

for T being non empty TopSpace

for F being Subset-Family of T holds

( ( for B being Subset of T st B in F holds

B c= Cl (union F) ) & ( for A being Subset of T st A is closed_condensed & ( for B being Subset of T st B in F holds

B c= A ) holds

Cl (union F) c= A ) )

for F being Subset-Family of T holds

( ( for B being Subset of T st B in F holds

B c= Cl (union F) ) & ( for A being Subset of T st A is closed_condensed & ( for B being Subset of T st B in F holds

B c= A ) holds

Cl (union F) c= A ) )

proof end;

theorem Th77: :: TDLAT_2:78

for T being non empty TopSpace

for F being Subset-Family of T holds

( ( F is closed implies for B being Subset of T st B in F holds

Cl (Int (meet F)) c= B ) & ( F = {} or for A being Subset of T st A is closed_condensed & ( for B being Subset of T st B in F holds

A c= B ) holds

A c= Cl (Int (meet F)) ) )

for F being Subset-Family of T holds

( ( F is closed implies for B being Subset of T st B in F holds

Cl (Int (meet F)) c= B ) & ( F = {} or for A being Subset of T st A is closed_condensed & ( for B being Subset of T st B in F holds

A c= B ) holds

A c= Cl (Int (meet F)) ) )

proof end;

definition

let T be non empty TopSpace;

let IT be Subset-Family of T;

end;
let IT be Subset-Family of T;

attr IT is open-domains-family means :: TDLAT_2:def 4

for A being Subset of T st A in IT holds

A is open_condensed ;

for A being Subset of T st A in IT holds

A is open_condensed ;

:: deftheorem defines open-domains-family TDLAT_2:def 4 :

for T being non empty TopSpace

for IT being Subset-Family of T holds

( IT is open-domains-family iff for A being Subset of T st A in IT holds

A is open_condensed );

for T being non empty TopSpace

for IT being Subset-Family of T holds

( IT is open-domains-family iff for A being Subset of T st A in IT holds

A is open_condensed );

theorem Th78: :: TDLAT_2:79

for T being non empty TopSpace

for F being Subset-Family of T holds

( F c= Open_Domains_of T iff F is open-domains-family )

for F being Subset-Family of T holds

( F c= Open_Domains_of T iff F is open-domains-family )

proof end;

theorem Th79: :: TDLAT_2:80

for T being non empty TopSpace

for F being Subset-Family of T st F is open-domains-family holds

F is domains-family

for F being Subset-Family of T st F is open-domains-family holds

F is domains-family

proof end;

theorem Th80: :: TDLAT_2:81

for T being non empty TopSpace

for F being Subset-Family of T st F is open-domains-family holds

F is open

for F being Subset-Family of T st F is open-domains-family holds

F is open

proof end;

theorem :: TDLAT_2:82

for T being non empty TopSpace

for F being Subset-Family of T st F is domains-family holds

Int F is open-domains-family

for F being Subset-Family of T st F is domains-family holds

Int F is open-domains-family

proof end;

theorem Th82: :: TDLAT_2:83

for T being non empty TopSpace

for F being Subset-Family of T st F is open-domains-family holds

( Int (meet F) is open_condensed & Int (Cl (union F)) is open_condensed )

for F being Subset-Family of T st F is open-domains-family holds

( Int (meet F) is open_condensed & Int (Cl (union F)) is open_condensed )

proof end;

theorem Th83: :: TDLAT_2:84

for T being non empty TopSpace

for F being Subset-Family of T holds

( ( F is open implies for B being Subset of T st B in F holds

B c= Int (Cl (union F)) ) & ( for A being Subset of T st A is open_condensed & ( for B being Subset of T st B in F holds

B c= A ) holds

Int (Cl (union F)) c= A ) )

for F being Subset-Family of T holds

( ( F is open implies for B being Subset of T st B in F holds

B c= Int (Cl (union F)) ) & ( for A being Subset of T st A is open_condensed & ( for B being Subset of T st B in F holds

B c= A ) holds

Int (Cl (union F)) c= A ) )

proof end;

theorem Th84: :: TDLAT_2:85

for T being non empty TopSpace

for F being Subset-Family of T holds

( ( for B being Subset of T st B in F holds

Int (meet F) c= B ) & ( F = {} or for A being Subset of T st A is open_condensed & ( for B being Subset of T st B in F holds

A c= B ) holds

A c= Int (meet F) ) )

for F being Subset-Family of T holds

( ( for B being Subset of T st B in F holds

Int (meet F) c= B ) & ( F = {} or for A being Subset of T st A is open_condensed & ( for B being Subset of T st B in F holds

A c= B ) holds

A c= Int (meet F) ) )

proof end;

theorem Th86: :: TDLAT_2:87

for T being non empty TopSpace

for a, b being Element of (Domains_Lattice T)

for A, B being Element of Domains_of T st a = A & b = B holds

( a "\/" b = (Int (Cl (A \/ B))) \/ (A \/ B) & a "/\" b = (Cl (Int (A /\ B))) /\ (A /\ B) )

for a, b being Element of (Domains_Lattice T)

for A, B being Element of Domains_of T st a = A & b = B holds

( a "\/" b = (Int (Cl (A \/ B))) \/ (A \/ B) & a "/\" b = (Cl (Int (A /\ B))) /\ (A /\ B) )

proof end;

theorem :: TDLAT_2:88

for T being non empty TopSpace holds

( Bottom (Domains_Lattice T) = {} T & Top (Domains_Lattice T) = [#] T )

( Bottom (Domains_Lattice T) = {} T & Top (Domains_Lattice T) = [#] T )

proof end;

theorem Th88: :: TDLAT_2:89

for T being non empty TopSpace

for a, b being Element of (Domains_Lattice T)

for A, B being Element of Domains_of T st a = A & b = B holds

( a [= b iff A c= B )

for a, b being Element of (Domains_Lattice T)

for A, B being Element of Domains_of T st a = A & b = B holds

( a [= b iff A c= B )

proof end;

theorem Th89: :: TDLAT_2:90

for T being non empty TopSpace

for X being Subset of (Domains_Lattice T) ex a being Element of (Domains_Lattice T) st

( X is_less_than a & ( for b being Element of (Domains_Lattice T) st X is_less_than b holds

a [= b ) )

for X being Subset of (Domains_Lattice T) ex a being Element of (Domains_Lattice T) st

( X is_less_than a & ( for b being Element of (Domains_Lattice T) st X is_less_than b holds

a [= b ) )

proof end;

theorem Th91: :: TDLAT_2:92

for T being non empty TopSpace

for F being Subset-Family of T st F is domains-family holds

for X being Subset of (Domains_Lattice T) st X = F holds

"\/" (X,(Domains_Lattice T)) = (union F) \/ (Int (Cl (union F)))

for F being Subset-Family of T st F is domains-family holds

for X being Subset of (Domains_Lattice T) st X = F holds

"\/" (X,(Domains_Lattice T)) = (union F) \/ (Int (Cl (union F)))

proof end;

theorem Th92: :: TDLAT_2:93

for T being non empty TopSpace

for F being Subset-Family of T st F is domains-family holds

for X being Subset of (Domains_Lattice T) st X = F holds

( ( X <> {} implies "/\" (X,(Domains_Lattice T)) = (meet F) /\ (Cl (Int (meet F))) ) & ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) )

for F being Subset-Family of T st F is domains-family holds

for X being Subset of (Domains_Lattice T) st X = F holds

( ( X <> {} implies "/\" (X,(Domains_Lattice T)) = (meet F) /\ (Cl (Int (meet F))) ) & ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) )

proof end;

::The Lattice of Closed Domains.

theorem Th93: :: TDLAT_2:94

for T being non empty TopSpace holds the carrier of (Closed_Domains_Lattice T) = Closed_Domains_of T

proof end;

theorem Th94: :: TDLAT_2:95

for T being non empty TopSpace

for a, b being Element of (Closed_Domains_Lattice T)

for A, B being Element of Closed_Domains_of T st a = A & b = B holds

( a "\/" b = A \/ B & a "/\" b = Cl (Int (A /\ B)) )

for a, b being Element of (Closed_Domains_Lattice T)

for A, B being Element of Closed_Domains_of T st a = A & b = B holds

( a "\/" b = A \/ B & a "/\" b = Cl (Int (A /\ B)) )

proof end;

theorem :: TDLAT_2:96

for T being non empty TopSpace holds

( Bottom (Closed_Domains_Lattice T) = {} T & Top (Closed_Domains_Lattice T) = [#] T )

( Bottom (Closed_Domains_Lattice T) = {} T & Top (Closed_Domains_Lattice T) = [#] T )

proof end;

theorem Th96: :: TDLAT_2:97

for T being non empty TopSpace

for a, b being Element of (Closed_Domains_Lattice T)

for A, B being Element of Closed_Domains_of T st a = A & b = B holds

( a [= b iff A c= B )

for a, b being Element of (Closed_Domains_Lattice T)

for A, B being Element of Closed_Domains_of T st a = A & b = B holds

( a [= b iff A c= B )

proof end;

theorem Th97: :: TDLAT_2:98

for T being non empty TopSpace

for X being Subset of (Closed_Domains_Lattice T) ex a being Element of (Closed_Domains_Lattice T) st

( X is_less_than a & ( for b being Element of (Closed_Domains_Lattice T) st X is_less_than b holds

a [= b ) )

for X being Subset of (Closed_Domains_Lattice T) ex a being Element of (Closed_Domains_Lattice T) st

( X is_less_than a & ( for b being Element of (Closed_Domains_Lattice T) st X is_less_than b holds

a [= b ) )

proof end;

theorem :: TDLAT_2:100

for T being non empty TopSpace

for F being Subset-Family of T st F is closed-domains-family holds

for X being Subset of (Closed_Domains_Lattice T) st X = F holds

"\/" (X,(Closed_Domains_Lattice T)) = Cl (union F)

for F being Subset-Family of T st F is closed-domains-family holds

for X being Subset of (Closed_Domains_Lattice T) st X = F holds

"\/" (X,(Closed_Domains_Lattice T)) = Cl (union F)

proof end;

theorem :: TDLAT_2:101

for T being non empty TopSpace

for F being Subset-Family of T st F is closed-domains-family holds

for X being Subset of (Closed_Domains_Lattice T) st X = F holds

( ( X <> {} implies "/\" (X,(Closed_Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Closed_Domains_Lattice T)) = [#] T ) )

for F being Subset-Family of T st F is closed-domains-family holds

for X being Subset of (Closed_Domains_Lattice T) st X = F holds

( ( X <> {} implies "/\" (X,(Closed_Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Closed_Domains_Lattice T)) = [#] T ) )

proof end;

theorem :: TDLAT_2:102

for T being non empty TopSpace

for F being Subset-Family of T st F is closed-domains-family holds

for X being Subset of (Domains_Lattice T) st X = F holds

( ( X <> {} implies "/\" (X,(Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) )

for F being Subset-Family of T st F is closed-domains-family holds

for X being Subset of (Domains_Lattice T) st X = F holds

( ( X <> {} implies "/\" (X,(Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) )

proof end;

::The Lattice of Open Domains.

theorem Th103: :: TDLAT_2:104

for T being non empty TopSpace

for a, b being Element of (Open_Domains_Lattice T)

for A, B being Element of Open_Domains_of T st a = A & b = B holds

( a "\/" b = Int (Cl (A \/ B)) & a "/\" b = A /\ B )

for a, b being Element of (Open_Domains_Lattice T)

for A, B being Element of Open_Domains_of T st a = A & b = B holds

( a "\/" b = Int (Cl (A \/ B)) & a "/\" b = A /\ B )

proof end;

theorem :: TDLAT_2:105

for T being non empty TopSpace holds

( Bottom (Open_Domains_Lattice T) = {} T & Top (Open_Domains_Lattice T) = [#] T )

( Bottom (Open_Domains_Lattice T) = {} T & Top (Open_Domains_Lattice T) = [#] T )

proof end;

theorem Th105: :: TDLAT_2:106

for T being non empty TopSpace

for a, b being Element of (Open_Domains_Lattice T)

for A, B being Element of Open_Domains_of T st a = A & b = B holds

( a [= b iff A c= B )

for a, b being Element of (Open_Domains_Lattice T)

for A, B being Element of Open_Domains_of T st a = A & b = B holds

( a [= b iff A c= B )

proof end;

theorem Th106: :: TDLAT_2:107

for T being non empty TopSpace

for X being Subset of (Open_Domains_Lattice T) ex a being Element of (Open_Domains_Lattice T) st

( X is_less_than a & ( for b being Element of (Open_Domains_Lattice T) st X is_less_than b holds

a [= b ) )

for X being Subset of (Open_Domains_Lattice T) ex a being Element of (Open_Domains_Lattice T) st

( X is_less_than a & ( for b being Element of (Open_Domains_Lattice T) st X is_less_than b holds

a [= b ) )

proof end;

theorem :: TDLAT_2:109

for T being non empty TopSpace

for F being Subset-Family of T st F is open-domains-family holds

for X being Subset of (Open_Domains_Lattice T) st X = F holds

"\/" (X,(Open_Domains_Lattice T)) = Int (Cl (union F))

for F being Subset-Family of T st F is open-domains-family holds

for X being Subset of (Open_Domains_Lattice T) st X = F holds

"\/" (X,(Open_Domains_Lattice T)) = Int (Cl (union F))

proof end;

theorem :: TDLAT_2:110

for T being non empty TopSpace

for F being Subset-Family of T st F is open-domains-family holds

for X being Subset of (Open_Domains_Lattice T) st X = F holds

( ( X <> {} implies "/\" (X,(Open_Domains_Lattice T)) = Int (meet F) ) & ( X = {} implies "/\" (X,(Open_Domains_Lattice T)) = [#] T ) )

for F being Subset-Family of T st F is open-domains-family holds

for X being Subset of (Open_Domains_Lattice T) st X = F holds

( ( X <> {} implies "/\" (X,(Open_Domains_Lattice T)) = Int (meet F) ) & ( X = {} implies "/\" (X,(Open_Domains_Lattice T)) = [#] T ) )

proof end;

theorem :: TDLAT_2:111

for T being non empty TopSpace

for F being Subset-Family of T st F is open-domains-family holds

for X being Subset of (Domains_Lattice T) st X = F holds

"\/" (X,(Domains_Lattice T)) = Int (Cl (union F))

for F being Subset-Family of T st F is open-domains-family holds

for X being Subset of (Domains_Lattice T) st X = F holds

"\/" (X,(Domains_Lattice T)) = Int (Cl (union F))

proof end;