:: Components and Basis of Topological Spaces
:: by Robert Milewski
::
:: Received June 22, 1999
:: Copyright (c) 1999-2012 Association of Mizar Users


begin

scheme :: YELLOW15:sch 1
SeqLambda1C{ F1() ->  Nat, F2() ->  non empty set , P1[ set ], F3( set ) ->  set , F4( set ) ->  set } :
 ex p being FinSequence of F2() st
( len p = F1() & ( for i being Nat st i in Seg F1() holds
( ( P1[i] implies p . i = F3(i) ) & ( P1[i] implies p . i = F4(i) ) ) ) )
provided
A1: for i being Nat st i in Seg F1() holds
( ( P1[i] implies F3(i) in F2() ) & ( P1[i] implies F4(i) in F2() ) )
proofend;

begin

definition
let X be set ;
let p be FinSequence of bool X;
let q be FinSequence of BOOLEAN ;
func MergeSequence (p,q) ->  FinSequence of bool X means :Def1: :: YELLOW15:def 1
( len it = len p & ( for i being Nat st i in dom p holds
it . i = IFEQ ((q . i),TRUE,(p . i),(X \ (p . i))) ) );
existence
 ex b1 being FinSequence of bool X st
( len b1 = len p & ( for i being Nat st i in dom p holds
b1 . i = IFEQ ((q . i),TRUE,(p . i),(X \ (p . i))) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of bool X st len b1 = len p & ( for i being Nat st i in dom p holds
b1 . i = IFEQ ((q . i),TRUE,(p . i),(X \ (p . i))) ) & len b2 = len p & ( for i being Nat st i in dom p holds
b2 . i = IFEQ ((q . i),TRUE,(p . i),(X \ (p . i))) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines MergeSequence YELLOW15:def_1_:_
 for X being set
for p being FinSequence of bool X
for q being FinSequence of BOOLEAN
for b4 being FinSequence of bool X holds
( b4 = MergeSequence (p,q) iff ( len b4 = len p & ( for i being Nat st i in dom p holds
b4 . i = IFEQ ((q . i),TRUE,(p . i),(X \ (p . i))) ) ) );

theorem :: YELLOW15:1
canceled;

theorem :: YELLOW15:2
canceled;

theorem :: YELLOW15:3
canceled;

theorem Th4: :: YELLOW15:4
for X being set
for p being FinSequence of bool X
for q being FinSequence of BOOLEAN holds dom (MergeSequence (p,q)) = dom p
proofend;

theorem Th5: :: YELLOW15:5
for X being set
for p being FinSequence of bool X
for q being FinSequence of BOOLEAN
for i being Nat st q . i = TRUE holds
(MergeSequence (p,q)) . i = p . i
proofend;

theorem Th6: :: YELLOW15:6
for X being set
for p being FinSequence of bool X
for q being FinSequence of BOOLEAN
for i being Nat st i in dom p & q . i = FALSE holds
(MergeSequence (p,q)) . i = X \ (p . i)
proofend;

theorem :: YELLOW15:7
for X being set
for q being FinSequence of BOOLEAN holds len (MergeSequence ((<*> (bool X)),q)) = 0
proofend;

theorem Th8: :: YELLOW15:8
for X being set
for q being FinSequence of BOOLEAN holds MergeSequence ((<*> (bool X)),q) = <*> (bool X)
proofend;

theorem :: YELLOW15:9
for X being set
for x being Subset of X
for q being FinSequence of BOOLEAN holds len (MergeSequence (<*x*>,q)) = 1
proofend;

theorem :: YELLOW15:10
for X being set
for x being Subset of X
for q being FinSequence of BOOLEAN holds
( ( q . 1 = TRUE implies (MergeSequence (<*x*>,q)) . 1 = x ) &amp; ( q . 1 = FALSE implies (MergeSequence (<*x*>,q)) . 1 = X \ x ) )
proofend;

theorem :: YELLOW15:11
for X being set
for x, y being Subset of X
for q being FinSequence of BOOLEAN holds len (MergeSequence (<*x,y*>,q)) = 2
proofend;

theorem :: YELLOW15:12
for X being set
for x, y being Subset of X
for q being FinSequence of BOOLEAN holds
( ( q . 1 = TRUE implies (MergeSequence (<*x,y*>,q)) . 1 = x ) &amp; ( q . 1 = FALSE implies (MergeSequence (<*x,y*>,q)) . 1 = X \ x ) &amp; ( q . 2 = TRUE implies (MergeSequence (<*x,y*>,q)) . 2 = y ) &amp; ( q . 2 = FALSE implies (MergeSequence (<*x,y*>,q)) . 2 = X \ y ) )
proofend;

theorem :: YELLOW15:13
for X being set
for x, y, z being Subset of X
for q being FinSequence of BOOLEAN holds len (MergeSequence (<*x,y,z*>,q)) = 3
proofend;

theorem :: YELLOW15:14
for X being set
for x, y, z being Subset of X
for q being FinSequence of BOOLEAN holds
( ( q . 1 = TRUE implies (MergeSequence (<*x,y,z*>,q)) . 1 = x ) &amp; ( q . 1 = FALSE implies (MergeSequence (<*x,y,z*>,q)) . 1 = X \ x ) &amp; ( q . 2 = TRUE implies (MergeSequence (<*x,y,z*>,q)) . 2 = y ) &amp; ( q . 2 = FALSE implies (MergeSequence (<*x,y,z*>,q)) . 2 = X \ y ) &amp; ( q . 3 = TRUE implies (MergeSequence (<*x,y,z*>,q)) . 3 = z ) &amp; ( q . 3 = FALSE implies (MergeSequence (<*x,y,z*>,q)) . 3 = X \ z ) )
proofend;

theorem Th15: :: YELLOW15:15
for X being set
for p being FinSequence of bool X holds  {  (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p  }  is Subset-Family of X
proofend;

registration
cluster  ->  boolean-valued for FinSequence of BOOLEAN ;
coherence
 for b1 being FinSequence of BOOLEAN holds b1 is boolean-valued
proofend;
end;

definition
let X be set ;
let Y be finite Subset-Family of X;
func Components Y ->  Subset-Family of X means :Def2: :: YELLOW15:def 2
 ex p being FinSequence of bool X st
( len p = card Y &amp; rng p = Y &amp; it =  {  (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p  }  );
existence
 ex b1 being Subset-Family of X ex p being FinSequence of bool X st
( len p = card Y &amp; rng p = Y &amp; b1 =  {  (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p  }  )
proofend;
uniqueness
 for b1, b2 being Subset-Family of X st ex p being FinSequence of bool X st
( len p = card Y &amp; rng p = Y &amp; b1 =  {  (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p  }  ) &amp; ex p being FinSequence of bool X st
( len p = card Y &amp; rng p = Y &amp; b2 =  {  (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p  }  ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines Components YELLOW15:def_2_:_
 for X being set
for Y being finite Subset-Family of X
for b3 being Subset-Family of X holds
( b3 = Components Y iff ex p being FinSequence of bool X st
( len p = card Y &amp; rng p = Y &amp; b3 =  {  (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p  }  ) );

registration
let X be set ;
let Y be finite Subset-Family of X;
cluster Components Y ->  finite ;
coherence
 Components Y is finite
proofend;
end;

theorem Th16: :: YELLOW15:16
for X being set
for Y being empty Subset-Family of X holds Components Y = {X}
proofend;

theorem :: YELLOW15:17
for X being set
for Y, Z being finite Subset-Family of X st Z c= Y holds
Components Y is_finer_than Components Z
proofend;

theorem Th18: :: YELLOW15:18
for X being set
for Y being finite Subset-Family of X holds union (Components Y) = X
proofend;

theorem Th19: :: YELLOW15:19
for X being set
for Y being finite Subset-Family of X
for A, B being set st A in Components Y &amp; B in Components Y &amp; A <> B holds
A misses B
proofend;

definition
let X be set ;
let Y be finite Subset-Family of X;
attrY is in_general_position  means :Def3: :: YELLOW15:def 3
 not {} in Components Y;
end;

:: deftheorem Def3 defines in_general_position YELLOW15:def_3_:_
 for X being set
for Y being finite Subset-Family of X holds
( Y is in_general_position iff not {} in Components Y );

theorem :: YELLOW15:20
for X being set
for Y, Z being finite Subset-Family of X st Z is in_general_position &amp; Y c= Z holds
Y is in_general_position
proofend;

theorem :: YELLOW15:21
for X being non empty set
for Y being empty Subset-Family of X holds Y is in_general_position
proofend;

theorem :: YELLOW15:22
for X being non empty set
for Y being finite Subset-Family of X st Y is in_general_position holds
Components Y is a_partition of X
proofend;

begin

theorem Th23: :: YELLOW15:23
for L being non empty RelStr holds
( [#] L is infs-closed &amp; [#] L is sups-closed )
proofend;

theorem Th24: :: YELLOW15:24
for L being non empty RelStr holds
( [#] L is with_bottom &amp; [#] L is with_top )
proofend;

registration
let L be non empty RelStr ;
cluster [#] L ->  infs-closed sups-closed with_bottom with_top ;
coherence
 ( [#] L is infs-closed &amp; [#] L is sups-closed &amp; [#] L is with_bottom &amp; [#] L is with_top ) by Th23, Th24;
end;

theorem :: YELLOW15:25
for L being continuous sup-Semilattice holds [#] L is CLbasis of L
proofend;

theorem :: YELLOW15:26
for L being non empty up-complete Poset st L is finite holds
the carrier of L = the carrier of (CompactSublatt L)
proofend;

theorem :: YELLOW15:27
for L being lower-bounded sup-Semilattice
for B being Subset of L st B is infinite holds
card B = card (finsups B)
proofend;

theorem :: YELLOW15:28
for T being non empty T_0 TopSpace holds card the carrier of T c= card the topology of T
proofend;

theorem Th29: :: YELLOW15:29
for T being TopStruct
for X being Subset of T st X is open holds
for B being finite Subset-Family of T st B is Basis of T holds
for Y being set holds
( not Y in Components B or X misses Y or Y c= X )
proofend;

theorem :: YELLOW15:30
for T being T_0 TopSpace st T is infinite holds
for B being Basis of T holds B is infinite
proofend;

theorem :: YELLOW15:31
for T being non empty TopSpace st T is finite holds
for B being Basis of T
for x being Element of T holds meet  {  A where A is Element of the topology of T : x in A  }  in B
proofend;