:: by Toshihiko Watanabe

::

:: Received June 12, 1992

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

theorem Th6: :: TDLAT_1:6

for T being TopSpace

for A, B being Subset of T st ( A is closed or B is closed ) holds

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

for A, B being Subset of T st ( A is closed or B is closed ) holds

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

proof end;

theorem Th7: :: TDLAT_1:7

for T being TopSpace

for A, B being Subset of T st ( A is open or B is open ) holds

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

for A, B being Subset of T st ( A is open or B is open ) holds

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

proof end;

theorem Th10: :: TDLAT_1:10

for T being TopSpace

for A, B being Subset of T holds (Int (Cl (A \/ ((Int (Cl B)) \/ B)))) \/ (A \/ ((Int (Cl B)) \/ B)) = (Int (Cl (A \/ B))) \/ (A \/ B)

for A, B being Subset of T holds (Int (Cl (A \/ ((Int (Cl B)) \/ B)))) \/ (A \/ ((Int (Cl B)) \/ B)) = (Int (Cl (A \/ B))) \/ (A \/ B)

proof end;

theorem :: TDLAT_1:11

theorem Th12: :: TDLAT_1:12

for T being TopSpace

for A, B being Subset of T holds (Cl (Int (A /\ ((Cl (Int B)) /\ B)))) /\ (A /\ ((Cl (Int B)) /\ B)) = (Cl (Int (A /\ B))) /\ (A /\ B)

for A, B being Subset of T holds (Cl (Int (A /\ ((Cl (Int B)) /\ B)))) /\ (A /\ ((Cl (Int B)) /\ B)) = (Cl (Int (A /\ B))) /\ (A /\ B)

proof end;

theorem :: TDLAT_1:13

:: 2. Properties of Domains_of of Topological Spaces.

theorem Th17: :: TDLAT_1:17

for T being TopSpace

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

( (Int (Cl (A \/ B))) \/ (A \/ B) is condensed & (Cl (Int (A /\ B))) /\ (A /\ B) is condensed )

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

( (Int (Cl (A \/ B))) \/ (A \/ B) is condensed & (Cl (Int (A /\ B))) /\ (A /\ B) is condensed )

proof end;

theorem :: TDLAT_1:26

theorem :: TDLAT_1:27

theorem Th28: :: TDLAT_1:28

for T being TopSpace

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

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

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

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

proof end;

theorem Th29: :: TDLAT_1:29

for T being TopSpace

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

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

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

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

proof end;

:: 3. The Lattice of Domains.

definition

let T be TopStruct ;

{ A where A is Subset of T : A is condensed } is Subset-Family of T

end;
func Domains_of T -> Subset-Family of T equals :: TDLAT_1:def 1

{ A where A is Subset of T : A is condensed } ;

coherence { A where A is Subset of T : A is condensed } ;

{ A where A is Subset of T : A is condensed } is Subset-Family of T

proof end;

:: deftheorem defines Domains_of TDLAT_1:def 1 :

for T being TopStruct holds Domains_of T = { A where A is Subset of T : A is condensed } ;

for T being TopStruct holds Domains_of T = { A where A is Subset of T : A is condensed } ;

definition

let T be TopSpace;

ex b_{1} being BinOp of (Domains_of T) st

for A, B being Element of Domains_of T holds b_{1} . (A,B) = (Int (Cl (A \/ B))) \/ (A \/ B)

for b_{1}, b_{2} being BinOp of (Domains_of T) st ( for A, B being Element of Domains_of T holds b_{1} . (A,B) = (Int (Cl (A \/ B))) \/ (A \/ B) ) & ( for A, B being Element of Domains_of T holds b_{2} . (A,B) = (Int (Cl (A \/ B))) \/ (A \/ B) ) holds

b_{1} = b_{2}

end;
func Domains_Union T -> BinOp of (Domains_of T) means :Def2: :: TDLAT_1:def 2

for A, B being Element of Domains_of T holds it . (A,B) = (Int (Cl (A \/ B))) \/ (A \/ B);

existence for A, B being Element of Domains_of T holds it . (A,B) = (Int (Cl (A \/ B))) \/ (A \/ B);

ex b

for A, B being Element of Domains_of T holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines Domains_Union TDLAT_1:def 2 :

for T being TopSpace

for b_{2} being BinOp of (Domains_of T) holds

( b_{2} = Domains_Union T iff for A, B being Element of Domains_of T holds b_{2} . (A,B) = (Int (Cl (A \/ B))) \/ (A \/ B) );

for T being TopSpace

for b

( b

definition

let T be TopSpace;

ex b_{1} being BinOp of (Domains_of T) st

for A, B being Element of Domains_of T holds b_{1} . (A,B) = (Cl (Int (A /\ B))) /\ (A /\ B)

for b_{1}, b_{2} being BinOp of (Domains_of T) st ( for A, B being Element of Domains_of T holds b_{1} . (A,B) = (Cl (Int (A /\ B))) /\ (A /\ B) ) & ( for A, B being Element of Domains_of T holds b_{2} . (A,B) = (Cl (Int (A /\ B))) /\ (A /\ B) ) holds

b_{1} = b_{2}

end;
func Domains_Meet T -> BinOp of (Domains_of T) means :Def3: :: TDLAT_1:def 3

for A, B being Element of Domains_of T holds it . (A,B) = (Cl (Int (A /\ B))) /\ (A /\ B);

existence for A, B being Element of Domains_of T holds it . (A,B) = (Cl (Int (A /\ B))) /\ (A /\ B);

ex b

for A, B being Element of Domains_of T holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines Domains_Meet TDLAT_1:def 3 :

for T being TopSpace

for b_{2} being BinOp of (Domains_of T) holds

( b_{2} = Domains_Meet T iff for A, B being Element of Domains_of T holds b_{2} . (A,B) = (Cl (Int (A /\ B))) /\ (A /\ B) );

for T being TopSpace

for b

( b

definition

let T be TopSpace;

LattStr(# (Domains_of T),(Domains_Union T),(Domains_Meet T) #) is C_Lattice by Th30;

end;
func Domains_Lattice T -> C_Lattice equals :: TDLAT_1:def 4

LattStr(# (Domains_of T),(Domains_Union T),(Domains_Meet T) #);

coherence LattStr(# (Domains_of T),(Domains_Union T),(Domains_Meet T) #);

LattStr(# (Domains_of T),(Domains_Union T),(Domains_Meet T) #) is C_Lattice by Th30;

:: deftheorem defines Domains_Lattice TDLAT_1:def 4 :

for T being TopSpace holds Domains_Lattice T = LattStr(# (Domains_of T),(Domains_Union T),(Domains_Meet T) #);

for T being TopSpace holds Domains_Lattice T = LattStr(# (Domains_of T),(Domains_Union T),(Domains_Meet T) #);

:: 4. The Lattice of Closed Domains.

definition

let T be TopStruct ;

{ A where A is Subset of T : A is closed_condensed } is Subset-Family of T

end;
func Closed_Domains_of T -> Subset-Family of T equals :: TDLAT_1:def 5

{ A where A is Subset of T : A is closed_condensed } ;

coherence { A where A is Subset of T : A is closed_condensed } ;

{ A where A is Subset of T : A is closed_condensed } is Subset-Family of T

proof end;

:: deftheorem defines Closed_Domains_of TDLAT_1:def 5 :

for T being TopStruct holds Closed_Domains_of T = { A where A is Subset of T : A is closed_condensed } ;

for T being TopStruct holds Closed_Domains_of T = { A where A is Subset of T : A is closed_condensed } ;

definition

let T be TopSpace;

ex b_{1} being BinOp of (Closed_Domains_of T) st

for A, B being Element of Closed_Domains_of T holds b_{1} . (A,B) = A \/ B

for b_{1}, b_{2} being BinOp of (Closed_Domains_of T) st ( for A, B being Element of Closed_Domains_of T holds b_{1} . (A,B) = A \/ B ) & ( for A, B being Element of Closed_Domains_of T holds b_{2} . (A,B) = A \/ B ) holds

b_{1} = b_{2}

end;
func Closed_Domains_Union T -> BinOp of (Closed_Domains_of T) means :Def6: :: TDLAT_1:def 6

for A, B being Element of Closed_Domains_of T holds it . (A,B) = A \/ B;

existence for A, B being Element of Closed_Domains_of T holds it . (A,B) = A \/ B;

ex b

for A, B being Element of Closed_Domains_of T holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def6 defines Closed_Domains_Union TDLAT_1:def 6 :

for T being TopSpace

for b_{2} being BinOp of (Closed_Domains_of T) holds

( b_{2} = Closed_Domains_Union T iff for A, B being Element of Closed_Domains_of T holds b_{2} . (A,B) = A \/ B );

for T being TopSpace

for b

( b

theorem Th32: :: TDLAT_1:32

for T being TopSpace

for A, B being Element of Closed_Domains_of T holds (CLD-Union T) . (A,B) = (D-Union T) . (A,B)

for A, B being Element of Closed_Domains_of T holds (CLD-Union T) . (A,B) = (D-Union T) . (A,B)

proof end;

definition

let T be TopSpace;

ex b_{1} being BinOp of (Closed_Domains_of T) st

for A, B being Element of Closed_Domains_of T holds b_{1} . (A,B) = Cl (Int (A /\ B))

for b_{1}, b_{2} being BinOp of (Closed_Domains_of T) st ( for A, B being Element of Closed_Domains_of T holds b_{1} . (A,B) = Cl (Int (A /\ B)) ) & ( for A, B being Element of Closed_Domains_of T holds b_{2} . (A,B) = Cl (Int (A /\ B)) ) holds

b_{1} = b_{2}

end;
func Closed_Domains_Meet T -> BinOp of (Closed_Domains_of T) means :Def7: :: TDLAT_1:def 7

for A, B being Element of Closed_Domains_of T holds it . (A,B) = Cl (Int (A /\ B));

existence for A, B being Element of Closed_Domains_of T holds it . (A,B) = Cl (Int (A /\ B));

ex b

for A, B being Element of Closed_Domains_of T holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def7 defines Closed_Domains_Meet TDLAT_1:def 7 :

for T being TopSpace

for b_{2} being BinOp of (Closed_Domains_of T) holds

( b_{2} = Closed_Domains_Meet T iff for A, B being Element of Closed_Domains_of T holds b_{2} . (A,B) = Cl (Int (A /\ B)) );

for T being TopSpace

for b

( b

theorem Th33: :: TDLAT_1:33

for T being TopSpace

for A, B being Element of Closed_Domains_of T holds (CLD-Meet T) . (A,B) = (D-Meet T) . (A,B)

for A, B being Element of Closed_Domains_of T holds (CLD-Meet T) . (A,B) = (D-Meet T) . (A,B)

proof end;

theorem Th34: :: TDLAT_1:34

for T being TopSpace holds LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #) is B_Lattice

proof end;

definition

let T be TopSpace;

LattStr(# (Closed_Domains_of T),(Closed_Domains_Union T),(Closed_Domains_Meet T) #) is B_Lattice by Th34;

end;
func Closed_Domains_Lattice T -> B_Lattice equals :: TDLAT_1:def 8

LattStr(# (Closed_Domains_of T),(Closed_Domains_Union T),(Closed_Domains_Meet T) #);

coherence LattStr(# (Closed_Domains_of T),(Closed_Domains_Union T),(Closed_Domains_Meet T) #);

LattStr(# (Closed_Domains_of T),(Closed_Domains_Union T),(Closed_Domains_Meet T) #) is B_Lattice by Th34;

:: deftheorem defines Closed_Domains_Lattice TDLAT_1:def 8 :

for T being TopSpace holds Closed_Domains_Lattice T = LattStr(# (Closed_Domains_of T),(Closed_Domains_Union T),(Closed_Domains_Meet T) #);

for T being TopSpace holds Closed_Domains_Lattice T = LattStr(# (Closed_Domains_of T),(Closed_Domains_Union T),(Closed_Domains_Meet T) #);

:: 5. The Lattice of Open Domains.

definition

let T be TopStruct ;

{ A where A is Subset of T : A is open_condensed } is Subset-Family of T

end;
func Open_Domains_of T -> Subset-Family of T equals :: TDLAT_1:def 9

{ A where A is Subset of T : A is open_condensed } ;

coherence { A where A is Subset of T : A is open_condensed } ;

{ A where A is Subset of T : A is open_condensed } is Subset-Family of T

proof end;

:: deftheorem defines Open_Domains_of TDLAT_1:def 9 :

for T being TopStruct holds Open_Domains_of T = { A where A is Subset of T : A is open_condensed } ;

for T being TopStruct holds Open_Domains_of T = { A where A is Subset of T : A is open_condensed } ;

definition

let T be TopSpace;

ex b_{1} being BinOp of (Open_Domains_of T) st

for A, B being Element of Open_Domains_of T holds b_{1} . (A,B) = Int (Cl (A \/ B))

for b_{1}, b_{2} being BinOp of (Open_Domains_of T) st ( for A, B being Element of Open_Domains_of T holds b_{1} . (A,B) = Int (Cl (A \/ B)) ) & ( for A, B being Element of Open_Domains_of T holds b_{2} . (A,B) = Int (Cl (A \/ B)) ) holds

b_{1} = b_{2}

end;
func Open_Domains_Union T -> BinOp of (Open_Domains_of T) means :Def10: :: TDLAT_1:def 10

for A, B being Element of Open_Domains_of T holds it . (A,B) = Int (Cl (A \/ B));

existence for A, B being Element of Open_Domains_of T holds it . (A,B) = Int (Cl (A \/ B));

ex b

for A, B being Element of Open_Domains_of T holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def10 defines Open_Domains_Union TDLAT_1:def 10 :

for T being TopSpace

for b_{2} being BinOp of (Open_Domains_of T) holds

( b_{2} = Open_Domains_Union T iff for A, B being Element of Open_Domains_of T holds b_{2} . (A,B) = Int (Cl (A \/ B)) );

for T being TopSpace

for b

( b

theorem Th36: :: TDLAT_1:36

for T being TopSpace

for A, B being Element of Open_Domains_of T holds (OPD-Union T) . (A,B) = (D-Union T) . (A,B)

for A, B being Element of Open_Domains_of T holds (OPD-Union T) . (A,B) = (D-Union T) . (A,B)

proof end;

definition

let T be TopSpace;

ex b_{1} being BinOp of (Open_Domains_of T) st

for A, B being Element of Open_Domains_of T holds b_{1} . (A,B) = A /\ B

for b_{1}, b_{2} being BinOp of (Open_Domains_of T) st ( for A, B being Element of Open_Domains_of T holds b_{1} . (A,B) = A /\ B ) & ( for A, B being Element of Open_Domains_of T holds b_{2} . (A,B) = A /\ B ) holds

b_{1} = b_{2}

end;
func Open_Domains_Meet T -> BinOp of (Open_Domains_of T) means :Def11: :: TDLAT_1:def 11

for A, B being Element of Open_Domains_of T holds it . (A,B) = A /\ B;

existence for A, B being Element of Open_Domains_of T holds it . (A,B) = A /\ B;

ex b

for A, B being Element of Open_Domains_of T holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def11 defines Open_Domains_Meet TDLAT_1:def 11 :

for T being TopSpace

for b_{2} being BinOp of (Open_Domains_of T) holds

( b_{2} = Open_Domains_Meet T iff for A, B being Element of Open_Domains_of T holds b_{2} . (A,B) = A /\ B );

for T being TopSpace

for b

( b

theorem Th37: :: TDLAT_1:37

for T being TopSpace

for A, B being Element of Open_Domains_of T holds (OPD-Meet T) . (A,B) = (D-Meet T) . (A,B)

for A, B being Element of Open_Domains_of T holds (OPD-Meet T) . (A,B) = (D-Meet T) . (A,B)

proof end;

definition

let T be TopSpace;

LattStr(# (Open_Domains_of T),(Open_Domains_Union T),(Open_Domains_Meet T) #) is B_Lattice by Th38;

end;
func Open_Domains_Lattice T -> B_Lattice equals :: TDLAT_1:def 12

LattStr(# (Open_Domains_of T),(Open_Domains_Union T),(Open_Domains_Meet T) #);

coherence LattStr(# (Open_Domains_of T),(Open_Domains_Union T),(Open_Domains_Meet T) #);

LattStr(# (Open_Domains_of T),(Open_Domains_Union T),(Open_Domains_Meet T) #) is B_Lattice by Th38;

:: deftheorem defines Open_Domains_Lattice TDLAT_1:def 12 :

for T being TopSpace holds Open_Domains_Lattice T = LattStr(# (Open_Domains_of T),(Open_Domains_Union T),(Open_Domains_Meet T) #);

for T being TopSpace holds Open_Domains_Lattice T = LattStr(# (Open_Domains_of T),(Open_Domains_Union T),(Open_Domains_Meet T) #);

:: 6. Connections between Lattices of Domains.