:: by Roland Coghetto

::

:: Received October 25, 2020

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

Lm1: for TX being non empty TopSpace

for O being open Subset of TX holds O is open Subset of (Top2NTop TX)

proof end;

Lm2: for NTX being NTopSpace holds

( [#] NTX is open & {} NTX is open )

proof end;

registration
end;

definition

let NTX be non empty strict U_FMT_filter FMT_Space_Str ;

let x be Element of NTX;

:: original: U_FMT

redefine func U_FMT x -> Filter of the carrier of NTX;

coherence

U_FMT x is Filter of the carrier of NTX by FINTOPO7:def 2;

end;
let x be Element of NTX;

:: original: U_FMT

redefine func U_FMT x -> Filter of the carrier of NTX;

coherence

U_FMT x is Filter of the carrier of NTX by FINTOPO7:def 2;

definition

let NTX be non empty strict U_FMT_filter FMT_Space_Str ;

let F be Filter of the carrier of NTX;

coherence

{ x where x is Point of NTX : F is_filter-finer_than U_FMT x } is Subset of NTX;

end;
let F be Filter of the carrier of NTX;

func lim_filter F -> Subset of NTX equals :: FINTOPO8:def 1

{ x where x is Point of NTX : F is_filter-finer_than U_FMT x } ;

correctness { x where x is Point of NTX : F is_filter-finer_than U_FMT x } ;

coherence

{ x where x is Point of NTX : F is_filter-finer_than U_FMT x } is Subset of NTX;

proof end;

:: deftheorem defines lim_filter FINTOPO8:def 1 :

for NTX being non empty strict U_FMT_filter FMT_Space_Str

for F being Filter of the carrier of NTX holds lim_filter F = { x where x is Point of NTX : F is_filter-finer_than U_FMT x } ;

for NTX being non empty strict U_FMT_filter FMT_Space_Str

for F being Filter of the carrier of NTX holds lim_filter F = { x where x is Point of NTX : F is_filter-finer_than U_FMT x } ;

definition

let NTX, NTY be non empty strict U_FMT_filter FMT_Space_Str ;

let f be Function of NTX,NTY;

let F be Filter of the carrier of NTX;

coherence

lim_filter (filter_image (f,F)) is Subset of NTY ;

end;
let f be Function of NTX,NTY;

let F be Filter of the carrier of NTX;

coherence

lim_filter (filter_image (f,F)) is Subset of NTY ;

:: deftheorem defines lim_filter FINTOPO8:def 2 :

for NTX, NTY being non empty strict U_FMT_filter FMT_Space_Str

for f being Function of NTX,NTY

for F being Filter of the carrier of NTX holds lim_filter (f,F) = lim_filter (filter_image (f,F));

for NTX, NTY being non empty strict U_FMT_filter FMT_Space_Str

for f being Function of NTX,NTY

for F being Filter of the carrier of NTX holds lim_filter (f,F) = lim_filter (filter_image (f,F));

:: deftheorem defines is_interior_point_of FINTOPO8:def 3 :

for NT being NTopSpace

for A being Subset of NT

for x being Point of NT holds

( x is_interior_point_of A iff A is a_neighborhood of x );

for NT being NTopSpace

for A being Subset of NT

for x being Point of NT holds

( x is_interior_point_of A iff A is a_neighborhood of x );

definition

let NT be NTopSpace;

let A be Subset of NT;

let x be Point of NT;

end;
let A be Subset of NT;

let x be Point of NT;

pred x is_adherent_point_of A means :: FINTOPO8:def 4

for V being Element of U_FMT x holds V meets A;

for V being Element of U_FMT x holds V meets A;

:: deftheorem defines is_adherent_point_of FINTOPO8:def 4 :

for NT being NTopSpace

for A being Subset of NT

for x being Point of NT holds

( x is_adherent_point_of A iff for V being Element of U_FMT x holds V meets A );

for NT being NTopSpace

for A being Subset of NT

for x being Point of NT holds

( x is_adherent_point_of A iff for V being Element of U_FMT x holds V meets A );

definition

let NT be NTopSpace;

let A be Subset of NT;

{ x where x is Point of NT : x is_interior_point_of A } is Subset of NT

end;
let A be Subset of NT;

func Int A -> Subset of NT equals :: FINTOPO8:def 5

{ x where x is Point of NT : x is_interior_point_of A } ;

coherence { x where x is Point of NT : x is_interior_point_of A } ;

{ x where x is Point of NT : x is_interior_point_of A } is Subset of NT

proof end;

:: deftheorem defines Int FINTOPO8:def 5 :

for NT being NTopSpace

for A being Subset of NT holds Int A = { x where x is Point of NT : x is_interior_point_of A } ;

for NT being NTopSpace

for A being Subset of NT holds Int A = { x where x is Point of NT : x is_interior_point_of A } ;

definition

let NTX, NTY be NTopSpace;

let f be Function of NTX,NTY;

let x be Point of NTX;

end;
let f be Function of NTX,NTY;

let x be Point of NTX;

pred f is_continuous_at x means :: FINTOPO8:def 6

for F being Filter of the carrier of NTX st x in lim_filter F holds

f . x in lim_filter (f,F);

for F being Filter of the carrier of NTX st x in lim_filter F holds

f . x in lim_filter (f,F);

:: deftheorem defines is_continuous_at FINTOPO8:def 6 :

for NTX, NTY being NTopSpace

for f being Function of NTX,NTY

for x being Point of NTX holds

( f is_continuous_at x iff for F being Filter of the carrier of NTX st x in lim_filter F holds

f . x in lim_filter (f,F) );

for NTX, NTY being NTopSpace

for f being Function of NTX,NTY

for x being Point of NTX holds

( f is_continuous_at x iff for F being Filter of the carrier of NTX st x in lim_filter F holds

f . x in lim_filter (f,F) );

:: deftheorem defines continuous FINTOPO8:def 7 :

for NTX, NTY being NTopSpace

for f being Function of NTX,NTY holds

( f is continuous iff for x being Point of NTX holds f is_continuous_at x );

for NTX, NTY being NTopSpace

for f being Function of NTX,NTY holds

( f is continuous iff for x being Point of NTX holds f is_continuous_at x );

Lm3: for NTX, NTY being NTopSpace

for a being Point of NTY holds NTX --> a is continuous

proof end;

registration

let NTX, NTY be NTopSpace;

ex b_{1} being Function of NTX,NTY st b_{1} is continuous

end;
cluster non empty V7() V10( the carrier of NTX) V11( the carrier of NTY) Function-like V27( the carrier of NTX) V31( the carrier of NTX, the carrier of NTY) continuous for Element of bool [: the carrier of NTX, the carrier of NTY:];

existence ex b

proof end;

Lm4: for NT being NTopSpace

for A being Subset of NT

for x being Point of NT holds

( x is_interior_point_of A iff ex O being open Subset of NT st

( x in O & O c= A ) )

proof end;

Lm5: for NT being NTopSpace

for A being Subset of NT holds Int A = union { O where O is open Subset of NT : O c= A }

proof end;

definition

let NT be NTopSpace;

let A be Subset of NT;

{ x where x is Point of NT : x is_adherent_point_of A } is Subset of NT

end;
let A be Subset of NT;

func Cl A -> Subset of NT equals :: FINTOPO8:def 8

{ x where x is Point of NT : x is_adherent_point_of A } ;

coherence { x where x is Point of NT : x is_adherent_point_of A } ;

{ x where x is Point of NT : x is_adherent_point_of A } is Subset of NT

proof end;

:: deftheorem defines Cl FINTOPO8:def 8 :

for NT being NTopSpace

for A being Subset of NT holds Cl A = { x where x is Point of NT : x is_adherent_point_of A } ;

for NT being NTopSpace

for A being Subset of NT holds Cl A = { x where x is Point of NT : x is_adherent_point_of A } ;

:: deftheorem Def9 defines closed FINTOPO8:def 9 :

for NTX being NTopSpace

for A being Subset of NTX holds

( A is closed iff ([#] NTX) \ A is open Subset of NTX );

for NTX being NTopSpace

for A being Subset of NTX holds

( A is closed iff ([#] NTX) \ A is open Subset of NTX );

registration
end;

registration

let NTX be NTopSpace;

coherence

for b_{1} being Subset of NTX st b_{1} = [#] NTX holds

b_{1} is closed

for b_{1} being Subset of NTX st b_{1} = {} NTX holds

b_{1} is closed
;

end;
coherence

for b

b

proof end;

coherence for b

b

registration

let NTX be NTopSpace;

existence

ex b_{1} being Subset of NTX st

( not b_{1} is empty & b_{1} is closed )

end;
existence

ex b

( not b

proof end;

definition

let S, T be non empty TopSpace;

let f be Function of S,T;

coherence

f is Function of (Top2NTop S),(Top2NTop T)

end;
let f be Function of S,T;

coherence

f is Function of (Top2NTop S),(Top2NTop T)

proof end;

:: deftheorem defines Top2NTop FINTOPO8:def 10 :

for S, T being non empty TopSpace

for f being Function of S,T holds Top2NTop f = f;

for S, T being non empty TopSpace

for f being Function of S,T holds Top2NTop f = f;

Lm6: for NT being NTopSpace

for A, B being Subset of NT st B = ([#] NT) \ A holds

( A is open iff B is closed )

proof end;

Lm7: for TX being non empty TopSpace

for F being closed Subset of TX holds F is closed Subset of (Top2NTop TX)

proof end;

Lm8: for NT being NTopSpace

for A, B being Subset of NT st A = ([#] NT) \ B holds

( A is open iff B is closed )

;

Lm9: for NTX being NTopSpace

for O being open Subset of NTX holds O is open Subset of (NTop2Top NTX)

proof end;

Lm10: for NTX being NTopSpace

for F being closed Subset of NTX holds F is closed Subset of (NTop2Top NTX)

proof end;

Lm11: for NTX, NTY being NTopSpace

for x being Point of NTX

for y being Point of NTY

for f being Function of NTX,NTY st f is_continuous_at x & y = f . x holds

for V being Element of U_FMT y ex W being Element of U_FMT x st f .: W c= V

proof end;

Lm12: for NTX, NTY being NTopSpace

for A being Subset of NTX

for B being Subset of NTY

for x being Point of NTX

for y being Point of NTY

for f being Function of NTX,NTY st f is_continuous_at x & x is_adherent_point_of A & y = f . x & B = f .: A holds

y is_adherent_point_of B

proof end;

Lm13: for NTX, NTY being NTopSpace

for A being Subset of NTX

for f being continuous Function of NTX,NTY holds f .: (Cl A) c= Cl (f .: A)

proof end;

Lm14: for NT being NTopSpace

for A, B being Subset of NT st B = ([#] NT) \ A holds

([#] NT) \ (Cl A) = Int B

proof end;

Lm15: for NT being NTopSpace

for A being Subset of NT holds Int A c= A

proof end;

Lm16: for NT being NTopSpace

for A being Subset of NT

for B being open Subset of NT st B c= A holds

B c= Int A

proof end;

Lm17: for NT being NTopSpace

for A, B being Subset of NT st A c= B holds

Int A c= Int B

proof end;

Lm18: for NT being NTopSpace

for A, B being Subset of NT st A c= B holds

Cl A c= Cl B

proof end;

Lm19: for NT being NTopSpace

for A being Subset of NT holds

( A is open iff Int A = A )

proof end;

Lm20: for NTX being NTopSpace

for A being closed Subset of NTX holds Cl A = A

proof end;

Lm21: for NT being NTopSpace

for A being Subset of NT holds A c= Cl A

proof end;

Lm22: for NTX being NTopSpace

for A being Subset of NTX st Cl A = A holds

A is closed Subset of NTX

proof end;

Lm23: for NTX, NTY being NTopSpace

for f being Function of NTX,NTY st ( for A being Subset of NTX holds f .: (Cl A) c= Cl (f .: A) ) holds

for S being closed Subset of NTY holds f " S is closed Subset of NTX

proof end;

Lm24: for NTX, NTY being NTopSpace

for f being Function of NTX,NTY st ( for S being closed Subset of NTY holds f " S is closed Subset of NTX ) holds

for S being open Subset of NTY holds f " S is open Subset of NTX

proof end;

Lm25: for NTX, NTY being NTopSpace

for x being Point of NTX

for y being Point of NTY

for f being Function of NTX,NTY st y = f . x & ( for V being Element of U_FMT y ex W being Element of U_FMT x st f .: W c= V ) holds

f is_continuous_at x

proof end;

Lm26: for NTX, NTY being NTopSpace

for f being Function of NTX,NTY st ( for S being open Subset of NTY holds f " S is open Subset of NTX ) holds

f is continuous

proof end;

Lm27: for NTX, NTY being NTopSpace

for f being Function of NTX,NTY holds

( f is continuous iff for O being closed Subset of NTY holds f " O is closed Subset of NTX )

proof end;

definition

let TX be non empty TopSpace;

let TY be non empty strict TopSpace;

let f be continuous Function of TX,TY;

coherence

Top2NTop f is continuous Function of (Top2NTop TX),(Top2NTop TY);

compatibility

for b_{1} being continuous Function of (Top2NTop TX),(Top2NTop TY) holds

( b_{1} = Top2NTop f iff b_{1} = f );

end;
let TY be non empty strict TopSpace;

let f be continuous Function of TX,TY;

:: original: Top2NTop

redefine func Top2NTop f -> continuous Function of (Top2NTop TX),(Top2NTop TY) equals :: FINTOPO8:def 11

f;

correctness redefine func Top2NTop f -> continuous Function of (Top2NTop TX),(Top2NTop TY) equals :: FINTOPO8:def 11

f;

coherence

Top2NTop f is continuous Function of (Top2NTop TX),(Top2NTop TY);

compatibility

for b

( b

proof end;

:: deftheorem defines Top2NTop FINTOPO8:def 11 :

for TX being non empty TopSpace

for TY being non empty strict TopSpace

for f being continuous Function of TX,TY holds Top2NTop f = f;

for TX being non empty TopSpace

for TY being non empty strict TopSpace

for f being continuous Function of TX,TY holds Top2NTop f = f;

definition

let NT be NTopSpace;

end;
attr NT is T_2 means :Def12: :: FINTOPO8:def 12

for F being Filter of the carrier of NT holds lim_filter F is trivial ;

for F being Filter of the carrier of NT holds lim_filter F is trivial ;

:: deftheorem Def12 defines T_2 FINTOPO8:def 12 :

for NT being NTopSpace holds

( NT is T_2 iff for F being Filter of the carrier of NT holds lim_filter F is trivial );

for NT being NTopSpace holds

( NT is T_2 iff for F being Filter of the carrier of NT holds lim_filter F is trivial );

definition

let NT be NTopSpace;

end;
attr NT is normal means :Def13: :: FINTOPO8:def 13

for A, B being closed Subset of NT st A misses B holds

ex V being a_neighborhood of A ex W being a_neighborhood of B st V misses W;

for A, B being closed Subset of NT st A misses B holds

ex V being a_neighborhood of A ex W being a_neighborhood of B st V misses W;

:: deftheorem Def13 defines normal FINTOPO8:def 13 :

for NT being NTopSpace holds

( NT is normal iff for A, B being closed Subset of NT st A misses B holds

ex V being a_neighborhood of A ex W being a_neighborhood of B st V misses W );

for NT being NTopSpace holds

( NT is normal iff for A, B being closed Subset of NT st A misses B holds

ex V being a_neighborhood of A ex W being a_neighborhood of B st V misses W );

Lm28: for T being non empty T_2 TopSpace holds Top2NTop T is T_2 NTopSpace

proof end;

Lm29: for NTX being NTopSpace

for A being closed Subset of NTX holds A is closed Subset of (NTop2Top NTX)

proof end;

definition
end;

:: deftheorem defines NTop2Top FINTOPO8:def 14 :

for NT being NTopSpace

for x being Point of NT holds NTop2Top x = x;

for NT being NTopSpace

for x being Point of NT holds NTop2Top x = x;

definition

let T be non empty TopSpace;

let x be Point of T;

coherence

x is Point of (Top2NTop T) by FINTOPO7:def 15;

end;
let x be Point of T;

coherence

x is Point of (Top2NTop T) by FINTOPO7:def 15;

:: deftheorem defines Top2NTop FINTOPO8:def 15 :

for T being non empty TopSpace

for x being Point of T holds Top2NTop x = x;

for T being non empty TopSpace

for x being Point of T holds Top2NTop x = x;

definition

let NT be NTopSpace;

let S be Subset of NT;

coherence

S is Subset of (NTop2Top NT) by FINTOPO7:def 16;

end;
let S be Subset of NT;

coherence

S is Subset of (NTop2Top NT) by FINTOPO7:def 16;

:: deftheorem defines NTop2Top FINTOPO8:def 16 :

for NT being NTopSpace

for S being Subset of NT holds NTop2Top S = S;

for NT being NTopSpace

for S being Subset of NT holds NTop2Top S = S;

definition

let T be non empty TopSpace;

let S be Subset of T;

coherence

S is Subset of (Top2NTop T) by FINTOPO7:def 15;

end;
let S be Subset of T;

coherence

S is Subset of (Top2NTop T) by FINTOPO7:def 15;

:: deftheorem defines Top2NTop FINTOPO8:def 17 :

for T being non empty TopSpace

for S being Subset of T holds Top2NTop S = S;

for T being non empty TopSpace

for S being Subset of T holds Top2NTop S = S;

Lm30: for T being non empty strict TopSpace

for A being Subset of T holds Int A = Int (Top2NTop A)

proof end;

Lm31: for T being non empty strict TopSpace

for A, B being Subset of T st A is a_neighborhood of B holds

Top2NTop A is a_neighborhood of Top2NTop B

proof end;

registration
end;

definition

let TX, TY be NTopSpace;

let f be Function of TX,TY;

coherence

f is Function of (NTop2Top TX),(NTop2Top TY)

end;
let f be Function of TX,TY;

coherence

f is Function of (NTop2Top TX),(NTop2Top TY)

proof end;

:: deftheorem defines NTop2Top FINTOPO8:def 18 :

for TX, TY being NTopSpace

for f being Function of TX,TY holds NTop2Top f = f;

for TX, TY being NTopSpace

for f being Function of TX,TY holds NTop2Top f = f;

theorem :: FINTOPO8:3

theorem :: FINTOPO8:4

for NT being NTopSpace

for A being Subset of NT holds A is Subset of (NTop2Top NT) by FINTOPO7:def 16;

for A being Subset of NT holds A is Subset of (NTop2Top NT) by FINTOPO7:def 16;

theorem :: FINTOPO8:6

theorem :: FINTOPO8:7

theorem :: FINTOPO8:8

theorem :: FINTOPO8:9

theorem :: FINTOPO8:11

theorem :: FINTOPO8:13

theorem Th14: :: FINTOPO8:14

for NT being NTopSpace

for A being Subset of NT

for x being Point of NT st A is a_neighborhood of x holds

Int A is open a_neighborhood of x

for A being Subset of NT

for x being Point of NT st A is a_neighborhood of x holds

Int A is open a_neighborhood of x

proof end;

theorem :: FINTOPO8:15

theorem :: FINTOPO8:16

theorem :: FINTOPO8:17

theorem :: FINTOPO8:18

theorem :: FINTOPO8:19

for NTX, NTY being NTopSpace

for XA being Subset of NTX

for YB being Subset of NTY

for x being Point of NTX

for y being Point of NTY

for f being Function of NTX,NTY st f is_continuous_at x & x is_adherent_point_of XA & y = f . x & YB = f .: XA holds

y is_adherent_point_of YB by Lm12;

for XA being Subset of NTX

for YB being Subset of NTY

for x being Point of NTX

for y being Point of NTY

for f being Function of NTX,NTY st f is_continuous_at x & x is_adherent_point_of XA & y = f . x & YB = f .: XA holds

y is_adherent_point_of YB by Lm12;

theorem :: FINTOPO8:20

theorem :: FINTOPO8:21

theorem :: FINTOPO8:22

theorem :: FINTOPO8:23

for NT being NTopSpace

for A, B being Subset of NT st B = ([#] NT) \ A holds

([#] NT) \ (Int A) = Cl B

for A, B being Subset of NT st B = ([#] NT) \ A holds

([#] NT) \ (Int A) = Cl B

proof end;

theorem :: FINTOPO8:25

theorem :: FINTOPO8:26

theorem :: FINTOPO8:27

theorem :: FINTOPO8:28

theorem :: FINTOPO8:29

theorem :: FINTOPO8:30

theorem :: FINTOPO8:31

theorem :: FINTOPO8:32

for NTX, NTY being NTopSpace

for f being Function of NTX,NTY holds

( f is continuous iff for O being open Subset of NTY holds f " O is open Subset of NTX )

for f being Function of NTX,NTY holds

( f is continuous iff for O being open Subset of NTY holds f " O is open Subset of NTX )

proof end;

theorem :: FINTOPO8:33

theorem :: FINTOPO8:35

for NT being NTopSpace

for A being Subset of NT

for a being Point of NT st A is a_neighborhood of a holds

NTop2Top A is a_neighborhood of NTop2Top a

for A being Subset of NT

for a being Point of NT st A is a_neighborhood of a holds

NTop2Top A is a_neighborhood of NTop2Top a

proof end;

theorem Th36: :: FINTOPO8:36

for NT being NTopSpace

for A, B being Subset of NT st A is a_neighborhood of B holds

NTop2Top A is a_neighborhood of NTop2Top B

for A, B being Subset of NT st A is a_neighborhood of B holds

NTop2Top A is a_neighborhood of NTop2Top B

proof end;

theorem :: FINTOPO8:37

theorem Th39: :: FINTOPO8:39

for NT being T_2 NTopSpace

for x, y being Point of NT st x <> y holds

ex Vx being Element of U_FMT x ex Vy being Element of U_FMT y st Vx misses Vy

for x, y being Point of NT st x <> y holds

ex Vx being Element of U_FMT x ex Vy being Element of U_FMT y st Vx misses Vy

proof end;

theorem :: FINTOPO8:42

theorem :: FINTOPO8:43

theorem :: FINTOPO8:44

theorem :: FINTOPO8:45

theorem :: FINTOPO8:46

theorem :: FINTOPO8:47

theorem :: FINTOPO8:48

for T being non empty strict TopSpace

for A, B being Subset of T st A is a_neighborhood of B holds

Top2NTop A is a_neighborhood of Top2NTop B by Lm31;

for A, B being Subset of T st A is a_neighborhood of B holds

Top2NTop A is a_neighborhood of Top2NTop B by Lm31;

theorem :: FINTOPO8:49

for T being non empty strict TopSpace

for A being Subset of T

for x being Point of T st A is a_neighborhood of x holds

Top2NTop A is a_neighborhood of Top2NTop x

for A being Subset of T

for x being Point of T st A is a_neighborhood of x holds

Top2NTop A is a_neighborhood of Top2NTop x

proof end;

theorem :: FINTOPO8:53

theorem :: FINTOPO8:54

theorem Th55: :: FINTOPO8:55

for A being Subset of FMT_R^1 holds

( A is open iff for x being Real st x in A holds

ex r being Real st

( r > 0 & ].(x - r),(x + r).[ c= A ) )

( A is open iff for x being Real st x in A holds

ex r being Real st

( r > 0 & ].(x - r),(x + r).[ c= A ) )

proof end;

theorem Th58: :: FINTOPO8:58

for x being Point of FMT_R^1

for r being Real st r > 0 holds

].(x - r),(x + r).[ is a_neighborhood of x

for r being Real st r > 0 holds

].(x - r),(x + r).[ is a_neighborhood of x

proof end;

theorem :: FINTOPO8:59

for x being object holds

( x is Point of FMT_R^1 iff x is Point of RealSpace ) by METRIC_1:def 13, TOPMETR:17, FINTOPO7:def 15;

( x is Point of FMT_R^1 iff x is Point of RealSpace ) by METRIC_1:def 13, TOPMETR:17, FINTOPO7:def 15;

theorem :: FINTOPO8:60

theorem Th61: :: FINTOPO8:61

for x being Point of FMT_R^1

for y being Point of RealSpace

for r being Real st x = y & r > 0 holds

Ball (y,r) is a_neighborhood of x

for y being Point of RealSpace

for r being Real st x = y & r > 0 holds

Ball (y,r) is a_neighborhood of x

proof end;

theorem :: FINTOPO8:62

for x being Point of FMT_R^1

for z being Point of (TopSpaceMetr RealSpace) st x = z holds

Balls z is Subset-Family of FMT_R^1 by FINTOPO7:def 15, TOPMETR:def 6;

for z being Point of (TopSpaceMetr RealSpace) st x = z holds

Balls z is Subset-Family of FMT_R^1 by FINTOPO7:def 15, TOPMETR:def 6;

theorem :: FINTOPO8:63

for x being Point of FMT_R^1

for z being Point of (TopSpaceMetr RealSpace)

for SF being Subset-Family of FMT_R^1 st x = z & SF = Balls z holds

<.SF.] = U_FMT x

for z being Point of (TopSpaceMetr RealSpace)

for SF being Subset-Family of FMT_R^1 st x = z & SF = Balls z holds

<.SF.] = U_FMT x

proof end;

definition

ex b_{1} being Function of the carrier of FMT_R^1,(bool (bool the carrier of FMT_R^1)) st

for r being Real ex x being Point of (TopSpaceMetr RealSpace) st

( x = r & b_{1} . r = Balls x )

for b_{1}, b_{2} being Function of the carrier of FMT_R^1,(bool (bool the carrier of FMT_R^1)) st ( for r being Real ex x being Point of (TopSpaceMetr RealSpace) st

( x = r & b_{1} . r = Balls x ) ) & ( for r being Real ex x being Point of (TopSpaceMetr RealSpace) st

( x = r & b_{2} . r = Balls x ) ) holds

b_{1} = b_{2}
end;

func gen_NS_R^1 -> Function of the carrier of FMT_R^1,(bool (bool the carrier of FMT_R^1)) means :Def20: :: FINTOPO8:def 20

for r being Real ex x being Point of (TopSpaceMetr RealSpace) st

( x = r & it . r = Balls x );

existence for r being Real ex x being Point of (TopSpaceMetr RealSpace) st

( x = r & it . r = Balls x );

ex b

for r being Real ex x being Point of (TopSpaceMetr RealSpace) st

( x = r & b

proof end;

uniqueness for b

( x = r & b

( x = r & b

b

proof end;

:: deftheorem Def20 defines gen_NS_R^1 FINTOPO8:def 20 :

for b_{1} being Function of the carrier of FMT_R^1,(bool (bool the carrier of FMT_R^1)) holds

( b_{1} = gen_NS_R^1 iff for r being Real ex x being Point of (TopSpaceMetr RealSpace) st

( x = r & b_{1} . r = Balls x ) );

for b

( b

( x = r & b

definition

FMT_Space_Str(# the carrier of FMT_R^1,gen_NS_R^1 #) is non empty strict FMT_Space_Str ;

end;

func gen_R^1 -> non empty strict FMT_Space_Str equals :: FINTOPO8:def 21

FMT_Space_Str(# the carrier of FMT_R^1,gen_NS_R^1 #);

coherence FMT_Space_Str(# the carrier of FMT_R^1,gen_NS_R^1 #);

FMT_Space_Str(# the carrier of FMT_R^1,gen_NS_R^1 #) is non empty strict FMT_Space_Str ;

:: deftheorem defines gen_R^1 FINTOPO8:def 21 :

gen_R^1 = FMT_Space_Str(# the carrier of FMT_R^1,gen_NS_R^1 #);

gen_R^1 = FMT_Space_Str(# the carrier of FMT_R^1,gen_NS_R^1 #);

theorem Th65: :: FINTOPO8:65

for x being Element of gen_R^1 ex y being Point of (TopSpaceMetr RealSpace) st

( x = y & U_FMT x = Balls y )

( x = y & U_FMT x = Balls y )

proof end;

theorem :: FINTOPO8:68

for NT being normal NTopSpace

for A, B being closed Subset of NT st A misses B holds

ex F being Function of NT,FMT_R^1 st

( F is continuous & ( for x being Point of NT holds

( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) )

for A, B being closed Subset of NT st A misses B holds

ex F being Function of NT,FMT_R^1 st

( F is continuous & ( for x being Point of NT holds

( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) )

proof end;