:: by Hiroshi Imura and Masayoshi Eguchi

::

:: Received November 27, 1992

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

theorem Th1: :: FIN_TOPO:1

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

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 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

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 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;

scheme :: FIN_TOPO:sch 1

MaxFinSeqEx{ F_{1}() -> non empty set , F_{2}() -> Subset of F_{1}(), F_{3}() -> Subset of F_{1}(), F_{4}( Subset of F_{1}()) -> Subset of F_{1}() } :

MaxFinSeqEx{ F

ex f being FinSequence of bool F_{1}() st

( len f > 0 & f /. 1 = F_{3}() & ( for i being Nat st i > 0 & i < len f holds

f /. (i + 1) = F_{4}((f /. i)) ) & F_{4}((f /. (len f))) = f /. (len f) & ( for i, j being Nat st i > 0 & i < j & j <= len f holds

( f /. i c= F_{2}() & f /. i c< f /. j ) ) )

provided( len f > 0 & f /. 1 = F

f /. (i + 1) = F

( f /. i c= F

A1:
F_{2}() is finite
and

A2: F_{3}() c= F_{2}()
and

A3: for A being Subset of F_{1}() st A c= F_{2}() holds

( A c= F_{4}(A) & F_{4}(A) c= F_{2}() )

A2: F

A3: for A being Subset of F

( A c= F

proof end;

registration
end;

definition

let FT be RelStr ;

let x be Element of FT;

coherence

Class ( the InternalRel of FT,x) is Subset of FT ;

end;
let x be Element of FT;

coherence

Class ( the InternalRel of FT,x) is Subset of FT ;

:: deftheorem defines U_FT FIN_TOPO:def 1 :

for FT being RelStr

for x being Element of FT holds U_FT x = Class ( the InternalRel of FT,x);

for FT being RelStr

for x being Element of FT holds U_FT x = Class ( the InternalRel of FT,x);

definition

let x be set ;

let y be Subset of {x};

:: original: .-->

redefine func x .--> y -> Function of {x},(bool {x});

coherence

x .--> y is Function of {x},(bool {x})

end;
let y be Subset of {x};

:: original: .-->

redefine func x .--> y -> Function of {x},(bool {x});

coherence

x .--> y is Function of {x},(bool {x})

proof end;

definition

let IT be non empty RelStr ;

( IT is filled iff for x being Element of IT holds x in U_FT x )

end;
redefine attr IT is reflexive means :Def4: :: FIN_TOPO:def 4

for x being Element of IT holds x in U_FT x;

compatibility for x being Element of IT holds x in U_FT x;

( IT is filled iff for x being Element of IT holds x in U_FT x )

proof end;

:: deftheorem Def4 defines filled FIN_TOPO:def 4 :

for IT being non empty RelStr holds

( IT is filled iff for x being Element of IT holds x in U_FT x );

for IT being non empty RelStr holds

( IT is filled iff for x being Element of IT holds x in U_FT x );

registration
end;

registration

existence

ex b_{1} being non empty RelStr st

( b_{1} is finite & b_{1} is filled & b_{1} is strict )
by Th3;

end;
ex b

( b

theorem :: FIN_TOPO:4

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

proof end;

definition

let FT be non empty RelStr ;

let A be Subset of FT;

{ x where x is Element of FT : ( U_FT x meets A & U_FT x meets A ` ) } is Subset of FT

end;
let A be Subset of FT;

func A ^delta -> Subset of FT equals :: FIN_TOPO:def 5

{ x where x is Element of FT : ( U_FT x meets A & U_FT x meets A ` ) } ;

coherence { x where x is Element of FT : ( U_FT x meets A & U_FT x meets A ` ) } ;

{ x where x is Element of FT : ( U_FT x meets A & U_FT x meets A ` ) } is Subset of FT

proof end;

:: deftheorem defines ^delta FIN_TOPO:def 5 :

for FT being non empty RelStr

for A being Subset of FT holds A ^delta = { x where x is Element of FT : ( U_FT x meets A & U_FT x meets A ` ) } ;

for FT being non empty RelStr

for A being Subset of FT holds A ^delta = { x where x is Element of FT : ( U_FT x meets A & U_FT x meets A ` ) } ;

theorem Th5: :: FIN_TOPO:5

for FT being non empty RelStr

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 ` ) )

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 RelStr ;

let A be Subset of FT;

coherence

A /\ (A ^delta) is Subset of FT ;

coherence

(A `) /\ (A ^delta) is Subset of FT ;

end;
let A be Subset of FT;

coherence

A /\ (A ^delta) is Subset of FT ;

coherence

(A `) /\ (A ^delta) is Subset of FT ;

:: deftheorem defines ^deltai FIN_TOPO:def 6 :

for FT being non empty RelStr

for A being Subset of FT holds A ^deltai = A /\ (A ^delta);

for FT being non empty RelStr

for A being Subset of FT holds A ^deltai = A /\ (A ^delta);

:: deftheorem defines ^deltao FIN_TOPO:def 7 :

for FT being non empty RelStr

for A being Subset of FT holds A ^deltao = (A `) /\ (A ^delta);

for FT being non empty RelStr

for A being Subset of FT holds A ^deltao = (A `) /\ (A ^delta);

definition

let FT be non empty RelStr ;

let A be Subset of FT;

coherence

{ x where x is Element of FT : U_FT x c= A } is Subset of FT

{ x where x is Element of FT : U_FT x meets A } is Subset of FT

{ x where x is Element of FT : ( x in A & (U_FT x) \ {x} misses A ) } is Subset of FT

end;
let A be Subset of FT;

coherence

{ x where x is Element of FT : U_FT x c= A } is Subset of FT

proof end;

func A ^b -> Subset of FT equals :: FIN_TOPO:def 9

{ x where x is Element of FT : U_FT x meets A } ;

coherence { x where x is Element of FT : U_FT x meets A } ;

{ x where x is Element of FT : U_FT x meets A } is Subset of FT

proof end;

func A ^s -> Subset of FT equals :: FIN_TOPO:def 10

{ x where x is Element of FT : ( x in A & (U_FT x) \ {x} misses A ) } ;

coherence { x where x is Element of FT : ( x in A & (U_FT x) \ {x} misses A ) } ;

{ x where x is Element of FT : ( x in A & (U_FT x) \ {x} misses A ) } is Subset of FT

proof end;

:: deftheorem defines ^i FIN_TOPO:def 8 :

for FT being non empty RelStr

for A being Subset of FT holds A ^i = { x where x is Element of FT : U_FT x c= A } ;

for FT being non empty RelStr

for A being Subset of FT holds A ^i = { x where x is Element of FT : U_FT x c= A } ;

:: deftheorem defines ^b FIN_TOPO:def 9 :

for FT being non empty RelStr

for A being Subset of FT holds A ^b = { x where x is Element of FT : U_FT x meets A } ;

for FT being non empty RelStr

for A being Subset of FT holds A ^b = { x where x is Element of FT : U_FT x meets A } ;

:: deftheorem defines ^s FIN_TOPO:def 10 :

for FT being non empty RelStr

for A being Subset of FT holds A ^s = { x where x is Element of FT : ( x in A & (U_FT x) \ {x} misses A ) } ;

for FT being non empty RelStr

for A being Subset of FT holds A ^s = { x where x is Element of FT : ( x in A & (U_FT x) \ {x} misses A ) } ;

definition

let FT be non empty RelStr ;

let A be Subset of FT;

coherence

A \ (A ^s) is Subset of FT ;

{ x where x is Element of FT : ex y being Element of FT st

( y in A & x in U_FT y ) } is Subset of FT

end;
let A be Subset of FT;

coherence

A \ (A ^s) is Subset of FT ;

func A ^f -> Subset of FT equals :: FIN_TOPO:def 12

{ x where x is Element of FT : ex y being Element of FT st

( y in A & x in U_FT y ) } ;

coherence { x where x is Element of FT : ex y being Element of FT st

( y in A & x in U_FT y ) } ;

{ x where x is Element of FT : ex y being Element of FT st

( y in A & x in U_FT y ) } is Subset of FT

proof end;

:: deftheorem defines ^n FIN_TOPO:def 11 :

for FT being non empty RelStr

for A being Subset of FT holds A ^n = A \ (A ^s);

for FT being non empty RelStr

for A being Subset of FT holds A ^n = A \ (A ^s);

:: deftheorem defines ^f FIN_TOPO:def 12 :

for FT being non empty RelStr

for A being Subset of FT holds A ^f = { x where x is Element of FT : ex y being Element of FT st

( y in A & x in U_FT y ) } ;

for FT being non empty RelStr

for A being Subset of FT holds A ^f = { x where x is Element of FT : ex y being Element of FT st

( y in A & x in U_FT y ) } ;

:: deftheorem defines symmetric FIN_TOPO:def 13 :

for IT being non empty RelStr holds

( IT is symmetric iff for x, y being Element of IT st y in U_FT x holds

x in U_FT y );

for IT being non empty RelStr holds

( IT is symmetric iff for x, y being Element of IT st y in U_FT x holds

x in U_FT y );

theorem Th7: :: FIN_TOPO:7

for FT being non empty RelStr

for x being Element of FT

for A being Subset of FT holds

( x in A ^i iff U_FT x c= A )

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 Th8: :: FIN_TOPO:8

for FT being non empty RelStr

for x being Element of FT

for A being Subset of FT holds

( x in A ^b iff U_FT x meets A )

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 Th9: :: FIN_TOPO:9

for FT being non empty RelStr

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 ) )

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:10

for FT being non empty RelStr

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 ) )

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 Th11: :: FIN_TOPO:11

for FT being non empty RelStr

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 ) )

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:12

for FT being non empty RelStr holds

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

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

proof end;

:: deftheorem defines open FIN_TOPO:def 14 :

for FT being non empty RelStr

for IT being Subset of FT holds

( IT is open iff IT = IT ^i );

for FT being non empty RelStr

for IT being Subset of FT holds

( IT is open iff IT = IT ^i );

:: deftheorem defines closed FIN_TOPO:def 15 :

for FT being non empty RelStr

for IT being Subset of FT holds

( IT is closed iff IT = IT ^b );

for FT being non empty RelStr

for IT being Subset of FT holds

( IT is closed iff IT = IT ^b );

:: deftheorem defines connected FIN_TOPO:def 16 :

for FT being non empty RelStr

for IT being Subset of FT holds

( IT is connected iff for B, C being Subset of FT st IT = B \/ C & B <> {} & C <> {} & B misses C holds

B ^b meets C );

for FT being non empty RelStr

for IT being Subset of FT holds

( IT is connected iff for B, C being Subset of FT st IT = B \/ C & B <> {} & C <> {} & B misses C holds

B ^b meets C );

definition

let FT be non empty RelStr ;

let A be Subset of FT;

meet { F where F is Subset of FT : ( A c= F & F is closed ) } is Subset of FT

union { F where F is Subset of FT : ( A c= F & F is open ) } is Subset of FT

end;
let A be Subset of FT;

func A ^fb -> Subset of FT equals :: FIN_TOPO:def 17

meet { F where F is Subset of FT : ( A c= F & F is closed ) } ;

coherence meet { F where F is Subset of FT : ( A c= F & F is closed ) } ;

meet { F where F is Subset of FT : ( A c= F & F is closed ) } is Subset of FT

proof end;

func A ^fi -> Subset of FT equals :: FIN_TOPO:def 18

union { F where F is Subset of FT : ( A c= F & F is open ) } ;

coherence union { F where F is Subset of FT : ( A c= F & F is open ) } ;

union { F where F is Subset of FT : ( A c= F & F is open ) } is Subset of FT

proof end;

:: deftheorem defines ^fb FIN_TOPO:def 17 :

for FT being non empty RelStr

for A being Subset of FT holds A ^fb = meet { F where F is Subset of FT : ( A c= F & F is closed ) } ;

for FT being non empty RelStr

for A being Subset of FT holds A ^fb = meet { F where F is Subset of FT : ( A c= F & F is closed ) } ;

:: deftheorem defines ^fi FIN_TOPO:def 18 :

for FT being non empty RelStr

for A being Subset of FT holds A ^fi = union { F where F is Subset of FT : ( A c= F & F is open ) } ;

for FT being non empty RelStr

for A being Subset of FT holds A ^fi = union { F where F is Subset of FT : ( A c= F & F is open ) } ;

theorem :: FIN_TOPO:15

for FT being non empty finite filled RelStr

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 Element of NAT st i > 0 & i < len S holds

S /. (i + 1) = ((S /. i) ^b) /\ A ) & A c= S /. (len S) ) )

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 Element of 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:20

for FT being non empty RelStr

for x being Element of FT

for A being Subset of FT st x in A ^s holds

not x in (A \ {x}) ^b

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:21

for FT being non empty RelStr

for A being Subset of FT st A ^s <> {} & card A <> 1 holds

not A is connected

for A being Subset of FT st A ^s <> {} & card A <> 1 holds

not A is connected

proof end;