:: by Gang Liu , Yasushi Fuwa and Masayoshi Eguchi

::

:: Received October 13, 2000

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

definition

let FT be non empty RelStr ;

let x, y be Element of FT;

let A be Subset of FT;

coherence

( ( y in U_FT x & y in A implies TRUE is Element of BOOLEAN ) & ( ( not y in U_FT x or not y in A ) implies FALSE is Element of BOOLEAN ) );

consistency

for b_{1} being Element of BOOLEAN holds verum;

;

end;
let x, y be Element of FT;

let A be Subset of FT;

func P_1 (x,y,A) -> Element of BOOLEAN equals :Def1: :: FINTOPO2:def 1

TRUE if ( y in U_FT x & y in A )

otherwise FALSE ;

correctness TRUE if ( y in U_FT x & y in A )

otherwise FALSE ;

coherence

( ( y in U_FT x & y in A implies TRUE is Element of BOOLEAN ) & ( ( not y in U_FT x or not y in A ) implies FALSE is Element of BOOLEAN ) );

consistency

for b

;

:: deftheorem Def1 defines P_1 FINTOPO2:def 1 :

for FT being non empty RelStr

for x, y being Element of FT

for A being Subset of FT holds

( ( y in U_FT x & y in A implies P_1 (x,y,A) = TRUE ) & ( ( not y in U_FT x or not y in A ) implies P_1 (x,y,A) = FALSE ) );

for FT being non empty RelStr

for x, y being Element of FT

for A being Subset of FT holds

( ( y in U_FT x & y in A implies P_1 (x,y,A) = TRUE ) & ( ( not y in U_FT x or not y in A ) implies P_1 (x,y,A) = FALSE ) );

definition

let FT be non empty RelStr ;

let x, y be Element of FT;

let A be Subset of FT;

coherence

( ( y in U_FT x & y in A ` implies TRUE is Element of BOOLEAN ) & ( ( not y in U_FT x or not y in A ` ) implies FALSE is Element of BOOLEAN ) );

consistency

for b_{1} being Element of BOOLEAN holds verum;

;

end;
let x, y be Element of FT;

let A be Subset of FT;

func P_2 (x,y,A) -> Element of BOOLEAN equals :Def2: :: FINTOPO2:def 2

TRUE if ( y in U_FT x & y in A ` )

otherwise FALSE ;

correctness TRUE if ( y in U_FT x & y in A ` )

otherwise FALSE ;

coherence

( ( y in U_FT x & y in A ` implies TRUE is Element of BOOLEAN ) & ( ( not y in U_FT x or not y in A ` ) implies FALSE is Element of BOOLEAN ) );

consistency

for b

;

:: deftheorem Def2 defines P_2 FINTOPO2:def 2 :

for FT being non empty RelStr

for x, y being Element of FT

for A being Subset of FT holds

( ( y in U_FT x & y in A ` implies P_2 (x,y,A) = TRUE ) & ( ( not y in U_FT x or not y in A ` ) implies P_2 (x,y,A) = FALSE ) );

for FT being non empty RelStr

for x, y being Element of FT

for A being Subset of FT holds

( ( y in U_FT x & y in A ` implies P_2 (x,y,A) = TRUE ) & ( ( not y in U_FT x or not y in A ` ) implies P_2 (x,y,A) = FALSE ) );

theorem :: FINTOPO2:6

theorem :: FINTOPO2:7

theorem Th8: :: FINTOPO2:8

for FT being non empty RelStr

for x being Element of FT

for A being Subset of FT holds

( x in A ^delta iff ex y1, y2 being Element of FT st

( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) )

for x being Element of FT

for A being Subset of FT holds

( x in A ^delta iff ex y1, y2 being Element of FT st

( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) )

proof end;

definition

let FT be non empty RelStr ;

let x, y be Element of FT;

coherence

( ( y in U_FT x implies TRUE is Element of BOOLEAN ) & ( not y in U_FT x implies FALSE is Element of BOOLEAN ) );

consistency

for b_{1} being Element of BOOLEAN holds verum;

;

end;
let x, y be Element of FT;

func P_0 (x,y) -> Element of BOOLEAN equals :Def3: :: FINTOPO2:def 3

TRUE if y in U_FT x

otherwise FALSE ;

correctness TRUE if y in U_FT x

otherwise FALSE ;

coherence

( ( y in U_FT x implies TRUE is Element of BOOLEAN ) & ( not y in U_FT x implies FALSE is Element of BOOLEAN ) );

consistency

for b

;

:: deftheorem Def3 defines P_0 FINTOPO2:def 3 :

for FT being non empty RelStr

for x, y being Element of FT holds

( ( y in U_FT x implies P_0 (x,y) = TRUE ) & ( not y in U_FT x implies P_0 (x,y) = FALSE ) );

for FT being non empty RelStr

for x, y being Element of FT holds

( ( y in U_FT x implies P_0 (x,y) = TRUE ) & ( not y in U_FT x implies P_0 (x,y) = FALSE ) );

theorem :: FINTOPO2:9

theorem :: FINTOPO2:10

for FT being non empty RelStr

for x being Element of FT

for A being Subset of FT holds

( x in A ^i iff for y being Element of FT st P_0 (x,y) = TRUE holds

P_1 (x,y,A) = TRUE )

for x being Element of FT

for A being Subset of FT holds

( x in A ^i iff for y being Element of FT st P_0 (x,y) = TRUE holds

P_1 (x,y,A) = TRUE )

proof end;

theorem :: FINTOPO2:11

for FT being non empty RelStr

for x being Element of FT

for A being Subset of FT holds

( x in A ^b iff ex y1 being Element of FT st P_1 (x,y1,A) = TRUE )

for x being Element of FT

for A being Subset of FT holds

( x in A ^b iff ex y1 being Element of FT st P_1 (x,y1,A) = TRUE )

proof end;

definition

let FT be non empty RelStr ;

let x be Element of FT;

let A be Subset of FT;

coherence

( ( x in A implies TRUE is Element of BOOLEAN ) & ( not x in A implies FALSE is Element of BOOLEAN ) );

consistency

for b_{1} being Element of BOOLEAN holds verum;

;

end;
let x be Element of FT;

let A be Subset of FT;

func P_A (x,A) -> Element of BOOLEAN equals :Def4: :: FINTOPO2:def 4

TRUE if x in A

otherwise FALSE ;

correctness TRUE if x in A

otherwise FALSE ;

coherence

( ( x in A implies TRUE is Element of BOOLEAN ) & ( not x in A implies FALSE is Element of BOOLEAN ) );

consistency

for b

;

:: deftheorem Def4 defines P_A FINTOPO2:def 4 :

for FT being non empty RelStr

for x being Element of FT

for A being Subset of FT holds

( ( x in A implies P_A (x,A) = TRUE ) & ( not x in A implies P_A (x,A) = FALSE ) );

for FT being non empty RelStr

for x being Element of FT

for A being Subset of FT holds

( ( x in A implies P_A (x,A) = TRUE ) & ( not x in A implies P_A (x,A) = FALSE ) );

theorem :: FINTOPO2:12

theorem :: FINTOPO2:13

for FT being non empty RelStr

for x being Element of FT

for A being Subset of FT holds

( x in A ^deltai iff ( ex y1, y2 being Element of FT st

( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = TRUE ) )

for x being Element of FT

for A being Subset of FT holds

( x in A ^deltai iff ( ex y1, y2 being Element of FT st

( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = TRUE ) )

proof end;

theorem :: FINTOPO2:14

for FT being non empty RelStr

for x being Element of FT

for A being Subset of FT holds

( x in A ^deltao iff ( ex y1, y2 being Element of FT st

( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = FALSE ) )

for x being Element of FT

for A being Subset of FT holds

( x in A ^deltao iff ( ex y1, y2 being Element of FT st

( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = FALSE ) )

proof end;

definition

let FT be non empty RelStr ;

let x, y be Element of FT;

coherence

( ( x = y implies TRUE is Element of BOOLEAN ) & ( not x = y implies FALSE is Element of BOOLEAN ) );

consistency

for b_{1} being Element of BOOLEAN holds verum;

;

end;
let x, y be Element of FT;

func P_e (x,y) -> Element of BOOLEAN equals :Def5: :: FINTOPO2:def 5

TRUE if x = y

otherwise FALSE ;

correctness TRUE if x = y

otherwise FALSE ;

coherence

( ( x = y implies TRUE is Element of BOOLEAN ) & ( not x = y implies FALSE is Element of BOOLEAN ) );

consistency

for b

;

:: deftheorem Def5 defines P_e FINTOPO2:def 5 :

for FT being non empty RelStr

for x, y being Element of FT holds

( ( x = y implies P_e (x,y) = TRUE ) & ( not x = y implies P_e (x,y) = FALSE ) );

for FT being non empty RelStr

for x, y being Element of FT holds

( ( x = y implies P_e (x,y) = TRUE ) & ( not x = y implies P_e (x,y) = FALSE ) );

theorem :: FINTOPO2:15

theorem :: FINTOPO2:16

for FT being non empty RelStr

for x being Element of FT

for A being Subset of FT holds

( x in A ^s iff ( P_A (x,A) = TRUE & ( for y being Element of FT holds

( not P_1 (x,y,A) = TRUE or not P_e (x,y) = FALSE ) ) ) )

for x being Element of FT

for A being Subset of FT holds

( x in A ^s iff ( P_A (x,A) = TRUE & ( for y being Element of FT holds

( not P_1 (x,y,A) = TRUE or not P_e (x,y) = FALSE ) ) ) )

proof end;

theorem :: FINTOPO2:17

for FT being non empty RelStr

for x being Element of FT

for A being Subset of FT holds

( x in A ^n iff ( P_A (x,A) = TRUE & ex y being Element of FT st

( P_1 (x,y,A) = TRUE & P_e (x,y) = FALSE ) ) )

for x being Element of FT

for A being Subset of FT holds

( x in A ^n iff ( P_A (x,A) = TRUE & ex y being Element of FT st

( P_1 (x,y,A) = TRUE & P_e (x,y) = FALSE ) ) )

proof end;

theorem :: FINTOPO2:18

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

( P_A (y,A) = TRUE & P_0 (y,x) = TRUE ) )

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

( P_A (y,A) = TRUE & P_0 (y,x) = TRUE ) )

proof end;

definition

attr c_{1} is strict ;

struct FMT_Space_Str -> 1-sorted ;

aggr FMT_Space_Str(# carrier, BNbd #) -> FMT_Space_Str ;

sel BNbd c_{1} -> Function of the carrier of c_{1},(bool (bool the carrier of c_{1}));

end;
struct FMT_Space_Str -> 1-sorted ;

aggr FMT_Space_Str(# carrier, BNbd #) -> FMT_Space_Str ;

sel BNbd c

registration
end;

definition

let FMT be non empty FMT_Space_Str ;

let x be Element of FMT;

correctness

coherence

the BNbd of FMT . x is Subset-Family of FMT;

;

end;
let x be Element of FMT;

correctness

coherence

the BNbd of FMT . x is Subset-Family of FMT;

;

:: deftheorem defines U_FMT FINTOPO2:def 6 :

for FMT being non empty FMT_Space_Str

for x being Element of FMT holds U_FMT x = the BNbd of FMT . x;

for FMT being non empty FMT_Space_Str

for x being Element of FMT holds U_FMT x = the BNbd of FMT . x;

definition

let T be non empty TopStruct ;

ex b_{1} being non empty strict FMT_Space_Str st

( the carrier of b_{1} = the carrier of T & ( for x being Point of b_{1} holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) )

for b_{1}, b_{2} being non empty strict FMT_Space_Str st the carrier of b_{1} = the carrier of T & ( for x being Point of b_{1} holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) & the carrier of b_{2} = the carrier of T & ( for x being Point of b_{2} holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) holds

b_{1} = b_{2}

end;
func NeighSp T -> non empty strict FMT_Space_Str means :: FINTOPO2:def 7

( the carrier of it = the carrier of T & ( for x being Point of it holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) );

existence ( the carrier of it = the carrier of T & ( for x being Point of it holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) );

ex b

( the carrier of b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defines NeighSp FINTOPO2:def 7 :

for T being non empty TopStruct

for b_{2} being non empty strict FMT_Space_Str holds

( b_{2} = NeighSp T iff ( the carrier of b_{2} = the carrier of T & ( for x being Point of b_{2} holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) ) );

for T being non empty TopStruct

for b

( b

:: deftheorem defines Fo_filled FINTOPO2:def 8 :

for IT being non empty FMT_Space_Str holds

( IT is Fo_filled iff for x being Element of IT

for D being Subset of IT st D in U_FMT x holds

x in D );

for IT being non empty FMT_Space_Str holds

( IT is Fo_filled iff for x being Element of IT

for D being Subset of IT st D in U_FMT x holds

x in D );

definition

let FMT be non empty FMT_Space_Str ;

let A be Subset of FMT;

{ x where x is Element of FMT : for W being Subset of FMT st W in U_FMT x holds

( W meets A & W meets A ` ) } is Subset of FMT

end;
let A be Subset of FMT;

func A ^Fodelta -> Subset of FMT equals :: FINTOPO2:def 9

{ x where x is Element of FMT : for W being Subset of FMT st W in U_FMT x holds

( W meets A & W meets A ` ) } ;

coherence { x where x is Element of FMT : for W being Subset of FMT st W in U_FMT x holds

( W meets A & W meets A ` ) } ;

{ x where x is Element of FMT : for W being Subset of FMT st W in U_FMT x holds

( W meets A & W meets A ` ) } is Subset of FMT

proof end;

:: deftheorem defines ^Fodelta FINTOPO2:def 9 :

for FMT being non empty FMT_Space_Str

for A being Subset of FMT holds A ^Fodelta = { x where x is Element of FMT : for W being Subset of FMT st W in U_FMT x holds

( W meets A & W meets A ` ) } ;

for FMT being non empty FMT_Space_Str

for A being Subset of FMT holds A ^Fodelta = { x where x is Element of FMT : for W being Subset of FMT st W in U_FMT x holds

( W meets A & W meets A ` ) } ;

theorem Th19: :: FINTOPO2:19

for FMT being non empty FMT_Space_Str

for x being Element of FMT

for A being Subset of FMT holds

( x in A ^Fodelta iff for W being Subset of FMT st W in U_FMT x holds

( W meets A & W meets A ` ) )

for x being Element of FMT

for A being Subset of FMT holds

( x in A ^Fodelta iff for W being Subset of FMT st W in U_FMT x holds

( W meets A & W meets A ` ) )

proof end;

definition

let FMT be non empty FMT_Space_Str ;

let A be Subset of FMT;

{ x where x is Element of FMT : for W being Subset of FMT st W in U_FMT x holds

W meets A } is Subset of FMT

end;
let A be Subset of FMT;

func A ^Fob -> Subset of FMT equals :: FINTOPO2:def 10

{ x where x is Element of FMT : for W being Subset of FMT st W in U_FMT x holds

W meets A } ;

coherence { x where x is Element of FMT : for W being Subset of FMT st W in U_FMT x holds

W meets A } ;

{ x where x is Element of FMT : for W being Subset of FMT st W in U_FMT x holds

W meets A } is Subset of FMT

proof end;

:: deftheorem defines ^Fob FINTOPO2:def 10 :

for FMT being non empty FMT_Space_Str

for A being Subset of FMT holds A ^Fob = { x where x is Element of FMT : for W being Subset of FMT st W in U_FMT x holds

W meets A } ;

for FMT being non empty FMT_Space_Str

for A being Subset of FMT holds A ^Fob = { x where x is Element of FMT : for W being Subset of FMT st W in U_FMT x holds

W meets A } ;

theorem Th20: :: FINTOPO2:20

for FMT being non empty FMT_Space_Str

for x being Element of FMT

for A being Subset of FMT holds

( x in A ^Fob iff for W being Subset of FMT st W in U_FMT x holds

W meets A )

for x being Element of FMT

for A being Subset of FMT holds

( x in A ^Fob iff for W being Subset of FMT st W in U_FMT x holds

W meets A )

proof end;

definition

let FMT be non empty FMT_Space_Str ;

let A be Subset of FMT;

{ x where x is Element of FMT : ex V being Subset of FMT st

( V in U_FMT x & V c= A ) } is Subset of FMT

end;
let A be Subset of FMT;

func A ^Foi -> Subset of FMT equals :: FINTOPO2:def 11

{ x where x is Element of FMT : ex V being Subset of FMT st

( V in U_FMT x & V c= A ) } ;

coherence { x where x is Element of FMT : ex V being Subset of FMT st

( V in U_FMT x & V c= A ) } ;

{ x where x is Element of FMT : ex V being Subset of FMT st

( V in U_FMT x & V c= A ) } is Subset of FMT

proof end;

:: deftheorem defines ^Foi FINTOPO2:def 11 :

for FMT being non empty FMT_Space_Str

for A being Subset of FMT holds A ^Foi = { x where x is Element of FMT : ex V being Subset of FMT st

( V in U_FMT x & V c= A ) } ;

for FMT being non empty FMT_Space_Str

for A being Subset of FMT holds A ^Foi = { x where x is Element of FMT : ex V being Subset of FMT st

( V in U_FMT x & V c= A ) } ;

theorem Th21: :: FINTOPO2:21

for FMT being non empty FMT_Space_Str

for x being Element of FMT

for A being Subset of FMT holds

( x in A ^Foi iff ex V being Subset of FMT st

( V in U_FMT x & V c= A ) )

for x being Element of FMT

for A being Subset of FMT holds

( x in A ^Foi iff ex V being Subset of FMT st

( V in U_FMT x & V c= A ) )

proof end;

definition

let FMT be non empty FMT_Space_Str ;

let A be Subset of FMT;

{ x where x is Element of FMT : ( x in A & ex V being Subset of FMT st

( V in U_FMT x & V \ {x} misses A ) ) } is Subset of FMT

end;
let A be Subset of FMT;

func A ^Fos -> Subset of FMT equals :: FINTOPO2:def 12

{ x where x is Element of FMT : ( x in A & ex V being Subset of FMT st

( V in U_FMT x & V \ {x} misses A ) ) } ;

coherence { x where x is Element of FMT : ( x in A & ex V being Subset of FMT st

( V in U_FMT x & V \ {x} misses A ) ) } ;

{ x where x is Element of FMT : ( x in A & ex V being Subset of FMT st

( V in U_FMT x & V \ {x} misses A ) ) } is Subset of FMT

proof end;

:: deftheorem defines ^Fos FINTOPO2:def 12 :

for FMT being non empty FMT_Space_Str

for A being Subset of FMT holds A ^Fos = { x where x is Element of FMT : ( x in A & ex V being Subset of FMT st

( V in U_FMT x & V \ {x} misses A ) ) } ;

for FMT being non empty FMT_Space_Str

for A being Subset of FMT holds A ^Fos = { x where x is Element of FMT : ( x in A & ex V being Subset of FMT st

( V in U_FMT x & V \ {x} misses A ) ) } ;

theorem Th22: :: FINTOPO2:22

for FMT being non empty FMT_Space_Str

for x being Element of FMT

for A being Subset of FMT holds

( x in A ^Fos iff ( x in A & ex V being Subset of FMT st

( V in U_FMT x & V \ {x} misses A ) ) )

for x being Element of FMT

for A being Subset of FMT holds

( x in A ^Fos iff ( x in A & ex V being Subset of FMT st

( V in U_FMT x & V \ {x} misses A ) ) )

proof end;

definition

let FMT be non empty FMT_Space_Str ;

let A be Subset of FMT;

coherence

A \ (A ^Fos) is Subset of FMT ;

end;
let A be Subset of FMT;

coherence

A \ (A ^Fos) is Subset of FMT ;

:: deftheorem defines ^Fon FINTOPO2:def 13 :

for FMT being non empty FMT_Space_Str

for A being Subset of FMT holds A ^Fon = A \ (A ^Fos);

for FMT being non empty FMT_Space_Str

for A being Subset of FMT holds A ^Fon = A \ (A ^Fos);

theorem :: FINTOPO2:23

for FMT being non empty FMT_Space_Str

for x being Element of FMT

for A being Subset of FMT holds

( x in A ^Fon iff ( x in A & ( for V being Subset of FMT st V in U_FMT x holds

V \ {x} meets A ) ) )

for x being Element of FMT

for A being Subset of FMT holds

( x in A ^Fon iff ( x in A & ( for V being Subset of FMT st V in U_FMT x holds

V \ {x} meets A ) ) )

proof end;

theorem Th26: :: FINTOPO2:26

for FMT being non empty FMT_Space_Str

for A, B being Subset of FMT holds (A ^Fob) \/ (B ^Fob) c= (A \/ B) ^Fob

for A, B being Subset of FMT holds (A ^Fob) \/ (B ^Fob) c= (A \/ B) ^Fob

proof end;

theorem :: FINTOPO2:27

for FMT being non empty FMT_Space_Str

for A, B being Subset of FMT holds (A /\ B) ^Fob c= (A ^Fob) /\ (B ^Fob)

for A, B being Subset of FMT holds (A /\ B) ^Fob c= (A ^Fob) /\ (B ^Fob)

proof end;

theorem :: FINTOPO2:28

for FMT being non empty FMT_Space_Str

for A, B being Subset of FMT holds (A ^Foi) \/ (B ^Foi) c= (A \/ B) ^Foi

for A, B being Subset of FMT holds (A ^Foi) \/ (B ^Foi) c= (A \/ B) ^Foi

proof end;

theorem Th29: :: FINTOPO2:29

for FMT being non empty FMT_Space_Str

for A, B being Subset of FMT holds (A /\ B) ^Foi c= (A ^Foi) /\ (B ^Foi)

for A, B being Subset of FMT holds (A /\ B) ^Foi c= (A ^Foi) /\ (B ^Foi)

proof end;

theorem :: FINTOPO2:30

for FMT being non empty FMT_Space_Str holds

( ( for x being Element of FMT

for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds

ex W being Subset of FMT st

( W in U_FMT x & W c= V1 /\ V2 ) ) iff for A, B being Subset of FMT holds (A \/ B) ^Fob = (A ^Fob) \/ (B ^Fob) )

( ( for x being Element of FMT

for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds

ex W being Subset of FMT st

( W in U_FMT x & W c= V1 /\ V2 ) ) iff for A, B being Subset of FMT holds (A \/ B) ^Fob = (A ^Fob) \/ (B ^Fob) )

proof end;

theorem :: FINTOPO2:31

for FMT being non empty FMT_Space_Str holds

( ( for x being Element of FMT

for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds

ex W being Subset of FMT st

( W in U_FMT x & W c= V1 /\ V2 ) ) iff for A, B being Subset of FMT holds (A ^Foi) /\ (B ^Foi) = (A /\ B) ^Foi )

( ( for x being Element of FMT

for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds

ex W being Subset of FMT st

( W in U_FMT x & W c= V1 /\ V2 ) ) iff for A, B being Subset of FMT holds (A ^Foi) /\ (B ^Foi) = (A /\ B) ^Foi )

proof end;

theorem :: FINTOPO2:32

for FMT being non empty FMT_Space_Str

for A, B being Subset of FMT st ( for x being Element of FMT

for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds

ex W being Subset of FMT st

( W in U_FMT x & W c= V1 /\ V2 ) ) holds

(A \/ B) ^Fodelta c= (A ^Fodelta) \/ (B ^Fodelta)

for A, B being Subset of FMT st ( for x being Element of FMT

for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds

ex W being Subset of FMT st

( W in U_FMT x & W c= V1 /\ V2 ) ) holds

(A \/ B) ^Fodelta c= (A ^Fodelta) \/ (B ^Fodelta)

proof end;

theorem :: FINTOPO2:33

for FMT being non empty FMT_Space_Str st FMT is Fo_filled & ( for A, B being Subset of FMT holds (A \/ B) ^Fodelta = (A ^Fodelta) \/ (B ^Fodelta) ) holds

for x being Element of FMT

for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds

ex W being Subset of FMT st

( W in U_FMT x & W c= V1 /\ V2 )

for x being Element of FMT

for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds

ex W being Subset of FMT st

( W in U_FMT x & W c= V1 /\ V2 )

proof end;

theorem :: FINTOPO2:34

for FMT being non empty FMT_Space_Str

for x being Element of FMT

for A being Subset of FMT holds

( x in A ^Fos iff ( x in A & not x in (A \ {x}) ^Fob ) )

for x being Element of FMT

for A being Subset of FMT holds

( x in A ^Fos iff ( x in A & not x in (A \ {x}) ^Fob ) )

proof end;

theorem Th35: :: FINTOPO2:35

for FMT being non empty FMT_Space_Str holds

( FMT is Fo_filled iff for A being Subset of FMT holds A c= A ^Fob )

( FMT is Fo_filled iff for A being Subset of FMT holds A c= A ^Fob )

proof end;

theorem Th36: :: FINTOPO2:36

for FMT being non empty FMT_Space_Str holds

( FMT is Fo_filled iff for A being Subset of FMT holds A ^Foi c= A )

( FMT is Fo_filled iff for A being Subset of FMT holds A ^Foi c= A )

proof end;

theorem Th39: :: FINTOPO2:39

for FMT being non empty FMT_Space_Str

for A being Subset of FMT holds A ^Fodelta = (A ^Fob) /\ ((A `) ^Fob)

for A being Subset of FMT holds A ^Fodelta = (A ^Fob) /\ ((A `) ^Fob)

proof end;

theorem :: FINTOPO2:40

for FMT being non empty FMT_Space_Str

for A being Subset of FMT holds A ^Fodelta = (A ^Fob) /\ ((A ^Foi) `)

for A being Subset of FMT holds A ^Fodelta = (A ^Fob) /\ ((A ^Foi) `)

proof end;

theorem :: FINTOPO2:42

for FMT being non empty FMT_Space_Str

for A being Subset of FMT holds A ^Fodelta = (A ^Fob) \ (A ^Foi)

for A being Subset of FMT holds A ^Fodelta = (A ^Fob) \ (A ^Foi)

proof end;

definition

let FMT be non empty FMT_Space_Str ;

let A be Subset of FMT;

coherence

A /\ (A ^Fodelta) is Subset of FMT ;

coherence

(A `) /\ (A ^Fodelta) is Subset of FMT ;

end;
let A be Subset of FMT;

coherence

A /\ (A ^Fodelta) is Subset of FMT ;

coherence

(A `) /\ (A ^Fodelta) is Subset of FMT ;

:: deftheorem defines ^Fodel_i FINTOPO2:def 14 :

for FMT being non empty FMT_Space_Str

for A being Subset of FMT holds A ^Fodel_i = A /\ (A ^Fodelta);

for FMT being non empty FMT_Space_Str

for A being Subset of FMT holds A ^Fodel_i = A /\ (A ^Fodelta);

:: deftheorem defines ^Fodel_o FINTOPO2:def 15 :

for FMT being non empty FMT_Space_Str

for A being Subset of FMT holds A ^Fodel_o = (A `) /\ (A ^Fodelta);

for FMT being non empty FMT_Space_Str

for A being Subset of FMT holds A ^Fodel_o = (A `) /\ (A ^Fodelta);

theorem :: FINTOPO2:43

for FMT being non empty FMT_Space_Str

for A being Subset of FMT holds A ^Fodelta = (A ^Fodel_i) \/ (A ^Fodel_o)

for A being Subset of FMT holds A ^Fodelta = (A ^Fodel_i) \/ (A ^Fodel_o)

proof end;

:: deftheorem defines Fo_open FINTOPO2:def 16 :

for FMT being non empty FMT_Space_Str

for G being Subset of FMT holds

( G is Fo_open iff G = G ^Foi );

for FMT being non empty FMT_Space_Str

for G being Subset of FMT holds

( G is Fo_open iff G = G ^Foi );

:: deftheorem defines Fo_closed FINTOPO2:def 17 :

for FMT being non empty FMT_Space_Str

for G being Subset of FMT holds

( G is Fo_closed iff G = G ^Fob );

for FMT being non empty FMT_Space_Str

for G being Subset of FMT holds

( G is Fo_closed iff G = G ^Fob );

theorem :: FINTOPO2:44

for FMT being non empty FMT_Space_Str

for A being Subset of FMT st A ` is Fo_open holds

A is Fo_closed

for A being Subset of FMT st A ` is Fo_open holds

A is Fo_closed

proof end;

theorem :: FINTOPO2:45

for FMT being non empty FMT_Space_Str

for A being Subset of FMT st A ` is Fo_closed holds

A is Fo_open

for A being Subset of FMT st A ` is Fo_closed holds

A is Fo_open

proof end;

theorem :: FINTOPO2:46

for FMT being non empty FMT_Space_Str

for A, B being Subset of FMT st FMT is Fo_filled & ( for x being Element of FMT holds {x} in U_FMT x ) holds

(A /\ B) ^Fob = (A ^Fob) /\ (B ^Fob)

for A, B being Subset of FMT st FMT is Fo_filled & ( for x being Element of FMT holds {x} in U_FMT x ) holds

(A /\ B) ^Fob = (A ^Fob) /\ (B ^Fob)

proof end;

theorem :: FINTOPO2:47

for FMT being non empty FMT_Space_Str

for A, B being Subset of FMT st FMT is Fo_filled & ( for x being Element of FMT holds {x} in U_FMT x ) holds

(A ^Foi) \/ (B ^Foi) = (A \/ B) ^Foi

for A, B being Subset of FMT st FMT is Fo_filled & ( for x being Element of FMT holds {x} in U_FMT x ) holds

(A ^Foi) \/ (B ^Foi) = (A \/ B) ^Foi

proof end;

:: SECTION2: Formal Topological Spaces

::