:: FIN_TOPO semantic presentation

for A being set
for f being FinSequence of bool A st ( for i being Nat st 1 <= i & i < len f holds
f /. i c= f /. (i + 1) ) holds
for i, j being Nat st i <= j & 1 <= i & j <= len f holds
f /. i c= f /. j

proof end;

theorem Th2: :: FIN_TOPO:2

for A being set
for f being FinSequence of bool A st ( for i being Nat st 1 <= i & i < len f holds
f /. i c= f /. (i + 1) ) holds
for i, j being Nat st i < j & 1 <= i & j <= len f & f /. j c= f /. i holds
for k being Nat st i <= k & k <= j holds
f /. j = f /. k

proof end;

Lm1: for f being Function st ( for i being Nat holds f . i c= f . (i + 1) ) holds
for i, j being Nat st i <= j holds
f . i c= f . j
by MEASURE2:22;

scheme :: FIN_TOPO:sch 1
MaxFinSeqEx{ F₁() -> non empty set , F₂() -> Subset of F₁(), F₃() -> Subset of F₁(), F₄( Subset of F₁()) -> Subset of F₁() } :

ex f being FinSequence of bool F₁() st
( len f > 0 & f /. 1 = F₃() & ( for i being Nat st i > 0 & i < len f holds
f /. (i + 1) = F₄((f /. i)) ) & F₄((f /. (len f))) = f /. (len f) & ( for i, j being Nat st i > 0 & i < j & j <= len f holds
( f /. i c= F₂() & f /. i c< f /. j ) ) )

provided

A1: F₂() is finite and
A2: F₃() c= F₂() and
A3: for A being Subset of F₁() st A c= F₂() holds
( A c= F₄(A) & F₄(A) c= F₂() )

proof end;

definition

attr c₁ is strict;
struct FT_Space_Str -> 1-sorted ;
aggr FT_Space_Str(# carrier, Nbd #) -> FT_Space_Str ;
sel Nbd c₁ -> Function of the carrier of c₁, bool the carrier of c₁;

end;

registration

cluster non empty strict FT_Space_Str ;
existence

proof end;

end;

definition

let FT be non empty FT_Space_Str ;
let x be Element of FT;
func U_FT x -> Subset of FT equals :: FIN_TOPO:def 1
the Nbd of FT . x;
coherence ;

end;

:: deftheorem defines U_FT FIN_TOPO:def 1 :

definition

let x be set ;
let y be Subset of {x};
:: original: .-->
redefine func x .--> y -> Function of {x}, bool {x};
coherence

proof end;

end;

definition

func FT{0} -> strict FT_Space_Str equals :: FIN_TOPO:def 2
FT_Space_Str(# {0},(0 .--> ([#] {0})) #);
coherence ;

end;

:: deftheorem defines FT{0} FIN_TOPO:def 2 :

registration

cluster FT{0} -> non empty strict ;
coherence

proof end;

end;

definition

let IT be non empty FT_Space_Str ;
attr IT is filled means :Def3: :: FIN_TOPO:def 3
for x being Element of IT holds x in U_FT x;

end;

:: deftheorem Def3 defines filled FIN_TOPO:def 3 :

theorem :: FIN_TOPO:3

canceled;

theorem :: FIN_TOPO:4

canceled;

theorem :: FIN_TOPO:5

canceled;

theorem :: FIN_TOPO:6

canceled;

theorem Th7: :: FIN_TOPO:7

FT{0} is filled

proof end;

theorem Th8: :: FIN_TOPO:8

FT{0} is finite

proof end;

registration

cluster non empty finite strict filled FT_Space_Str ;
existence by Th7, Th8;

end;

definition

let T be 1-sorted ;
let F be set ;
canceled;
pred F is_a_cover_of T means :: FIN_TOPO:def 5
the carrier of T c= union F;

end;

:: deftheorem FIN_TOPO:def 4 :

:: deftheorem defines is_a_cover_of FIN_TOPO:def 5 :

theorem :: FIN_TOPO:9

for FT being non empty filled FT_Space_Str holds { (U_FT x) where x is Element of FT : verum } is_a_cover_of FT

proof end;

definition

let FT be non empty FT_Space_Str ;
let A be Subset of FT;
func A ^delta -> Subset of FT equals :: FIN_TOPO:def 6
{ x where x is Element of FT : ( U_FT x meets A & U_FT x meets A ` ) } ;
coherence

proof end;

end;

:: deftheorem defines ^delta FIN_TOPO:def 6 :

theorem Th10: :: FIN_TOPO:10

for FT being non empty FT_Space_Str
for x being Element of FT
for A being Subset of FT holds
( x in A ^delta iff ( U_FT x meets A & U_FT x meets A ` ) )

proof end;

definition

let FT be non empty FT_Space_Str ;
let A be Subset of FT;
func A ^deltai -> Subset of FT equals :: FIN_TOPO:def 7
A /\ (A ^delta );
coherence ;
func A ^deltao -> Subset of FT equals :: FIN_TOPO:def 8
(A ` ) /\ (A ^delta );
coherence ;

end;

:: deftheorem defines ^deltai FIN_TOPO:def 7 :

:: deftheorem defines ^deltao FIN_TOPO:def 8 :

theorem :: FIN_TOPO:11

for FT being non empty FT_Space_Str
for A being Subset of FT holds A ^delta = (A ^deltai ) \/ (A ^deltao )

proof end;

definition

let FT be non empty FT_Space_Str ;
let A be Subset of FT;
func A ^i -> Subset of FT equals :: FIN_TOPO:def 9
{ x where x is Element of FT : U_FT x c= A } ;
coherence

proof end;

func A ^b -> Subset of FT equals :: FIN_TOPO:def 10
{ x where x is Element of FT : U_FT x meets A } ;
coherence

proof end;

func A ^s -> Subset of FT equals :: FIN_TOPO:def 11
{ x where x is Element of FT : ( x in A & (U_FT x) \ {x} misses A ) } ;
coherence

proof end;

end;

:: deftheorem defines ^i FIN_TOPO:def 9 :

:: deftheorem defines ^b FIN_TOPO:def 10 :

:: deftheorem defines ^s FIN_TOPO:def 11 :

definition

let FT be non empty FT_Space_Str ;
let A be Subset of FT;
func A ^n -> Subset of FT equals :: FIN_TOPO:def 12
A \ (A ^s );
coherence ;
func A ^f -> Subset of FT equals :: FIN_TOPO:def 13
{ x where x is Element of FT : ex y being Element of FT st
( y in A & x in U_FT y ) } ;
coherence

proof end;

end;

:: deftheorem defines ^n FIN_TOPO:def 12 :

:: deftheorem defines ^f FIN_TOPO:def 13 :

definition

let IT be non empty FT_Space_Str ;
attr IT is symmetric means :Def14: :: FIN_TOPO:def 14
for x, y being Element of IT st y in U_FT x holds
x in U_FT y;

end;

:: deftheorem Def14 defines symmetric FIN_TOPO:def 14 :

theorem Th12: :: FIN_TOPO:12

for FT being non empty FT_Space_Str
for x being Element of FT
for A being Subset of FT holds
( x in A ^i iff U_FT x c= A )

proof end;

theorem Th13: :: FIN_TOPO:13

for FT being non empty FT_Space_Str
for x being Element of FT
for A being Subset of FT holds
( x in A ^b iff U_FT x meets A )

proof end;

theorem Th14: :: FIN_TOPO:14

for FT being non empty FT_Space_Str
for x being Element of FT
for A being Subset of FT holds
( x in A ^s iff ( x in A & (U_FT x) \ {x} misses A ) )

proof end;

theorem :: FIN_TOPO:15

for FT being non empty FT_Space_Str
for x being Element of FT
for A being Subset of FT holds
( x in A ^n iff ( x in A & (U_FT x) \ {x} meets A ) )

proof end;

theorem Th16: :: FIN_TOPO:16

for FT being non empty FT_Space_Str
for x being Element of FT
for A being Subset of FT holds
( x in A ^f iff ex y being Element of FT st
( y in A & x in U_FT y ) )

proof end;

theorem :: FIN_TOPO:17

for FT being non empty FT_Space_Str holds
( FT is symmetric iff for A being Subset of FT holds A ^b = A ^f )

proof end;

definition

let FT be non empty FT_Space_Str ;
let IT be Subset of FT;
attr IT is open means :Def15: :: FIN_TOPO:def 15
IT = IT ^i ;
attr IT is closed means :Def16: :: FIN_TOPO:def 16
IT = IT ^b ;
attr IT is connected means :Def17: :: FIN_TOPO:def 17
for B, C being Subset of FT st IT = B \/ C & B <> {} & C <> {} & B misses C holds
B ^b meets C;

end;

:: deftheorem Def15 defines open FIN_TOPO:def 15 :

:: deftheorem Def16 defines closed FIN_TOPO:def 16 :

:: deftheorem Def17 defines connected FIN_TOPO:def 17 :

definition

let FT be non empty FT_Space_Str ;
let A be Subset of FT;
func A ^fb -> Subset of FT equals :: FIN_TOPO:def 18
meet { F where F is Subset of FT : ( A c= F & F is closed ) } ;
coherence

proof end;

func A ^fi -> Subset of FT equals :: FIN_TOPO:def 19
union { F where F is Subset of FT : ( A c= F & F is open ) } ;
coherence

proof end;

end;

:: deftheorem defines ^fb FIN_TOPO:def 18 :

:: deftheorem defines ^fi FIN_TOPO:def 19 :

theorem Th18: :: FIN_TOPO:18

for FT being non empty filled FT_Space_Str
for A being Subset of FT holds A c= A ^b

proof end;

theorem Th19: :: FIN_TOPO:19

for FT being non empty FT_Space_Str
for A, B being Subset of FT st A c= B holds
A ^b c= B ^b

proof end;

theorem :: FIN_TOPO:20

for FT being non empty finite filled FT_Space_Str
for A being Subset of FT holds
( A is connected iff for x being Element of FT st x in A holds
ex S being FinSequence of bool the carrier of FT st
( len S > 0 & S /. 1 = {x} & ( for i being Nat st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b ) /\ A ) & A c= S /. (len S) ) )

proof end;

theorem :: FIN_TOPO:21

for E being non empty set
for A being Subset of E
for x being Element of E holds
( x in A ` iff not x in A ) by SUBSET_1:50, SUBSET_1:54;

theorem Th22: :: FIN_TOPO:22

for FT being non empty FT_Space_Str
for A being Subset of FT holds ((A ` ) ^i ) ` = A ^b

proof end;

theorem Th23: :: FIN_TOPO:23

for FT being non empty FT_Space_Str
for A being Subset of FT holds ((A ` ) ^b ) ` = A ^i

proof end;

theorem :: FIN_TOPO:24

for FT being non empty FT_Space_Str
for A being Subset of FT holds A ^delta = (A ^b ) /\ ((A ` ) ^b )

proof end;

theorem :: FIN_TOPO:25

for FT being non empty FT_Space_Str
for A being Subset of FT holds (A ` ) ^delta = A ^delta

proof end;

theorem :: FIN_TOPO:26

for FT being non empty FT_Space_Str
for x being Element of FT
for A being Subset of FT st x in A ^s holds
not x in (A \ {x}) ^b

proof end;

theorem :: FIN_TOPO:27

for FT being non empty FT_Space_Str
for A being Subset of FT st A ^s <> {} & Card A <> 1 holds
not A is connected

proof end;

theorem :: FIN_TOPO:28

for FT being non empty filled FT_Space_Str
for A being Subset of FT holds A ^i c= A

proof end;

theorem :: FIN_TOPO:29

for E being set
for A, B being Subset of E holds
( A = B iff A ` = B ` )

proof end;

theorem :: FIN_TOPO:30

for FT being non empty FT_Space_Str
for A being Subset of FT st A is open holds
A ` is closed

proof end;

theorem :: FIN_TOPO:31

for FT being non empty FT_Space_Str
for A being Subset of FT st A is closed holds
A ` is open

proof end;