:: FIN_TOPO semantic presentation

theorem Th1: :: FIN_TOPO:1

for b₁ being set
for b₂ being FinSequence of bool b₁ st ( for b₃ being Nat st 1 <= b₃ & b₃ < len b₂ holds
b₂ /. b₃ c= b₂ /. (b₃ + 1) ) holds
for b₃, b₄ being Nat st b₃ <= b₄ & 1 <= b₃ & b₄ <= len b₂ holds
b₂ /. b₃ c= b₂ /. b₄

proof end;

theorem Th2: :: FIN_TOPO:2

for b₁ being set
for b₂ being FinSequence of bool b₁ st ( for b₃ being Nat st 1 <= b₃ & b₃ < len b₂ holds
b₂ /. b₃ c= b₂ /. (b₃ + 1) ) holds
for b₃, b₄ being Nat st b₃ < b₄ & 1 <= b₃ & b₄ <= len b₂ & b₂ /. b₄ c= b₂ /. b₃ holds
for b₅ being Nat st b₃ <= b₅ & b₅ <= b₄ holds
b₂ /. b₄ = b₂ /. b₅

proof end;

Lemma3: for b₁ being Function st ( for b₂ being Nat holds b₁ . b₂ c= b₁ . (b₂ + 1) ) holds
for b₂, b₃ being Nat st b₂ <= b₃ holds
b₁ . b₂ c= b₁ . b₃
by MEASURE2:22;

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

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

provided

E4: F₂() is finite and
E5: F₃() c= F₂() and
E6: for b₁ being Subset of F₁() st b₁ c= F₂() holds
( b₁ c= F₄(b₁) & F₄(b₁) c= F₂() )

proof end;

definition

attr a₁ 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 a₁, bool the carrier of a₁;

end;

registration

cluster non empty strict FT_Space_Str ;
existence

proof end;

end;

definition

let c₁ be non empty FT_Space_Str ;
let c₂ be Element of c₁;
func U_FT c₂ -> Subset of a₁ equals :: FIN_TOPO:def 1
the Nbd of a₁ . a₂;
coherence ;

end;

:: deftheorem Def1 defines U_FT FIN_TOPO:def 1 :

definition

let c₁ be set ;
let c₂ be Subset of {c₁};
redefine func .--> as c₁ .--> c₂ -> Function of {a₁}, bool {a₁};
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 Def2 defines FT{0} FIN_TOPO:def 2 :

registration

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

proof end;

end;

definition

let c₁ be non empty FT_Space_Str ;
attr a₁ is filled means :Def3: :: FIN_TOPO:def 3
for b₁ being Element of a₁ holds b₁ in U_FT b₁;

end;

:: deftheorem Def3 defines filled FIN_TOPO:def 3 :

theorem Th3: :: FIN_TOPO:3

canceled;

theorem Th4: :: FIN_TOPO:4

canceled;

theorem Th5: :: FIN_TOPO:5

canceled;

theorem Th6: :: 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 c₁ be 1-sorted ;
let c₂ be set ;
canceled;
pred c₂ is_a_cover_of c₁ means :: FIN_TOPO:def 5
the carrier of a₁ c= union a₂;

end;

:: deftheorem Def4 FIN_TOPO:def 4 :

:: deftheorem Def5 defines is_a_cover_of FIN_TOPO:def 5 :

theorem Th9: :: FIN_TOPO:9

for b₁ being non empty filled FT_Space_Str holds { (U_FT b₂) where B is Element of b₁ : verum } is_a_cover_of b₁

proof end;

definition

let c₁ be non empty FT_Space_Str ;
let c₂ be Subset of c₁;
func c₂ ^delta -> Subset of a₁ equals :: FIN_TOPO:def 6
{ b₁ where B is Element of a₁ : ( U_FT b₁ meets a₂ & U_FT b₁ meets a₂ ` ) } ;
coherence

proof end;

end;

:: deftheorem Def6 defines ^delta FIN_TOPO:def 6 :

theorem Th10: :: FIN_TOPO:10

for b₁ being non empty FT_Space_Str
for b₂ being Element of b₁
for b₃ being Subset of b₁ holds
( b₂ in b₃ ^delta iff ( U_FT b₂ meets b₃ & U_FT b₂ meets b₃ ` ) )

proof end;

definition

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

end;

:: deftheorem Def7 defines ^deltai FIN_TOPO:def 7 :

:: deftheorem Def8 defines ^deltao FIN_TOPO:def 8 :

theorem Th11: :: FIN_TOPO:11

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁ holds b₂ ^delta = (b₂ ^deltai ) \/ (b₂ ^deltao )

proof end;

definition

let c₁ be non empty FT_Space_Str ;
let c₂ be Subset of c₁;
func c₂ ^i -> Subset of a₁ equals :: FIN_TOPO:def 9
{ b₁ where B is Element of a₁ : U_FT b₁ c= a₂ } ;
coherence

proof end;

func c₂ ^b -> Subset of a₁ equals :: FIN_TOPO:def 10
{ b₁ where B is Element of a₁ : U_FT b₁ meets a₂ } ;
coherence

proof end;

func c₂ ^s -> Subset of a₁ equals :: FIN_TOPO:def 11
{ b₁ where B is Element of a₁ : ( b₁ in a₂ & (U_FT b₁) \ {b₁} misses a₂ ) } ;
coherence

proof end;

end;

:: deftheorem Def9 defines ^i FIN_TOPO:def 9 :

:: deftheorem Def10 defines ^b FIN_TOPO:def 10 :

:: deftheorem Def11 defines ^s FIN_TOPO:def 11 :

definition

let c₁ be non empty FT_Space_Str ;
let c₂ be Subset of c₁;
func c₂ ^n -> Subset of a₁ equals :: FIN_TOPO:def 12
a₂ \ (a₂ ^s );
coherence ;
func c₂ ^f -> Subset of a₁ equals :: FIN_TOPO:def 13
{ b₁ where B is Element of a₁ : ex b₁ being Element of a₁ st
( b₂ in a₂ & b₁ in U_FT b₂ ) } ;
coherence

proof end;

end;

:: deftheorem Def12 defines ^n FIN_TOPO:def 12 :

:: deftheorem Def13 defines ^f FIN_TOPO:def 13 :

definition

let c₁ be non empty FT_Space_Str ;
attr a₁ is symmetric means :Def14: :: FIN_TOPO:def 14
for b₁, b₂ being Element of a₁ st b₂ in U_FT b₁ holds
b₁ in U_FT b₂;

end;

:: deftheorem Def14 defines symmetric FIN_TOPO:def 14 :

theorem Th12: :: FIN_TOPO:12

for b₁ being non empty FT_Space_Str
for b₂ being Element of b₁
for b₃ being Subset of b₁ holds
( b₂ in b₃ ^i iff U_FT b₂ c= b₃ )

proof end;

theorem Th13: :: FIN_TOPO:13

for b₁ being non empty FT_Space_Str
for b₂ being Element of b₁
for b₃ being Subset of b₁ holds
( b₂ in b₃ ^b iff U_FT b₂ meets b₃ )

proof end;

theorem Th14: :: FIN_TOPO:14

for b₁ being non empty FT_Space_Str
for b₂ being Element of b₁
for b₃ being Subset of b₁ holds
( b₂ in b₃ ^s iff ( b₂ in b₃ & (U_FT b₂) \ {b₂} misses b₃ ) )

proof end;

theorem Th15: :: FIN_TOPO:15

for b₁ being non empty FT_Space_Str
for b₂ being Element of b₁
for b₃ being Subset of b₁ holds
( b₂ in b₃ ^n iff ( b₂ in b₃ & (U_FT b₂) \ {b₂} meets b₃ ) )

proof end;

theorem Th16: :: FIN_TOPO:16

for b₁ being non empty FT_Space_Str
for b₂ being Element of b₁
for b₃ being Subset of b₁ holds
( b₂ in b₃ ^f iff ex b₄ being Element of b₁ st
( b₄ in b₃ & b₂ in U_FT b₄ ) )

proof end;

theorem Th17: :: FIN_TOPO:17

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

proof end;

definition

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

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 c₁ be non empty FT_Space_Str ;
let c₂ be Subset of c₁;
func c₂ ^fb -> Subset of a₁ equals :: FIN_TOPO:def 18
meet { b₁ where B is Subset of a₁ : ( a₂ c= b₁ & b₁ is closed ) } ;
coherence

proof end;

func c₂ ^fi -> Subset of a₁ equals :: FIN_TOPO:def 19
union { b₁ where B is Subset of a₁ : ( a₂ c= b₁ & b₁ is open ) } ;
coherence

proof end;

end;

:: deftheorem Def18 defines ^fb FIN_TOPO:def 18 :

:: deftheorem Def19 defines ^fi FIN_TOPO:def 19 :

theorem Th18: :: FIN_TOPO:18

for b₁ being non empty filled FT_Space_Str
for b₂ being Subset of b₁ holds b₂ c= b₂ ^b

proof end;

theorem Th19: :: FIN_TOPO:19

for b₁ being non empty FT_Space_Str
for b₂, b₃ being Subset of b₁ st b₂ c= b₃ holds
b₂ ^b c= b₃ ^b

proof end;

theorem Th20: :: FIN_TOPO:20

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

proof end;

theorem Th21: :: FIN_TOPO:21

for b₁ being non empty set
for b₂ being Subset of b₁
for b₃ being Element of b₁ holds
( b₃ in b₂ ` iff not b₃ in b₂ ) by SUBSET_1:50, SUBSET_1:54;

theorem Th22: :: FIN_TOPO:22

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁ holds ((b₂ ` ) ^i ) ` = b₂ ^b

proof end;

theorem Th23: :: FIN_TOPO:23

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁ holds ((b₂ ` ) ^b ) ` = b₂ ^i

proof end;

theorem Th24: :: FIN_TOPO:24

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

proof end;

theorem Th25: :: FIN_TOPO:25

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁ holds (b₂ ` ) ^delta = b₂ ^delta

proof end;

theorem Th26: :: FIN_TOPO:26

for b₁ being non empty FT_Space_Str
for b₂ being Element of b₁
for b₃ being Subset of b₁ st b₂ in b₃ ^s holds
not b₂ in (b₃ \ {b₂}) ^b

proof end;

theorem Th27: :: FIN_TOPO:27

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

proof end;

theorem Th28: :: FIN_TOPO:28

for b₁ being non empty filled FT_Space_Str
for b₂ being Subset of b₁ holds b₂ ^i c= b₂

proof end;

theorem Th29: :: FIN_TOPO:29

for b₁ being set
for b₂, b₃ being Subset of b₁ holds
( b₂ = b₃ iff b₂ ` = b₃ ` )

proof end;

theorem Th30: :: FIN_TOPO:30

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁ st b₂ is open holds
b₂ ` is closed

proof end;

theorem Th31: :: FIN_TOPO:31

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁ st b₂ is closed holds
b₂ ` is open

proof end;