:: A Case Study of Transport Urysohn's Lemma from TopSpace Defined with Open Sets to TopSpace Defined with Neighborhoods
:: by Roland Coghetto
::
:: Received October 25, 2020
:: Copyright (c) 2020-2021 Association of Mizar Users

theorem Th1: :: FINTOPO8:1

for T being TopSpace
for A, B being Subset of T st A misses B holds
Int A misses Int B

proof end;

definition

mode NTopSpace is FMT_TopSpace;

end;

notation

let X be non empty TopSpace;
synonym Top2NTop X for TopSpace2FMT X;

end;

notation

let X be FMT_TopSpace;
synonym NTop2Top X for FMT2TopSpace X;

end;

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

let NTX be NTopSpace;

cluster [#] NTX -> open ;

coherence
[#] NTX is open by Lm2;

cluster {} NTX -> open ;

coherence
{} NTX is open by Lm2;

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;

definition

let NTX be non empty strict U_FMT_filter FMT_Space_Str ;
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
coherence
{ x where x is Point of NTX : F is_filter-finer_than U_FMT x } is Subset of NTX;

proof end;

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

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;

func lim_filter (f,F) -> Subset of NTY equals :: FINTOPO8:def 2
lim_filter (filter_image (f,F));

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

end;

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

definition

let NT be NTopSpace;
let A be Subset of NT;
let x be Point of NT;

pred x is_interior_point_of A means :: FINTOPO8:def 3
A is a_neighborhood of x;

end;

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

definition

let NT be NTopSpace;
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;

end;

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

definition

let NT be NTopSpace;
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 } is Subset of NT

proof end;

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

definition

let NTX, NTY be NTopSpace;
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);

end;

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

definition

let NTX, NTY be NTopSpace;
let f be Function of NTX,NTY;

attr f is continuous means :: FINTOPO8:def 7
for x being Point of NTX holds f is_continuous_at x;

end;

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

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;

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₁ being Function of NTX,NTY st b₁ is continuous

proof end;

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;

registration

let NT be NTopSpace;
let A be Subset of NT;

cluster Int A -> open ;

coherence
Int A is open

proof end;

end;

definition

let NT be NTopSpace;
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 } is Subset of NT

proof end;

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

definition

let NTX be NTopSpace;
let A be Subset of NTX;

attr A is closed means :Def9: :: FINTOPO8:def 9
([#] NTX) \ A is open Subset of NTX;

end;

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

registration

let NTX be NTopSpace;

cluster closed for Element of bool the carrier of NTX;

existence
ex b₁ being Subset of NTX st b₁ is closed

proof end;

end;

registration

let NTX be NTopSpace;

cluster [#] NTX -> closed for Subset of NTX;

coherence
for b₁ being Subset of NTX st b₁ = [#] NTX holds
b₁ is closed

proof end;

cluster {} NTX -> closed for Subset of NTX;

coherence
for b₁ being Subset of NTX st b₁ = {} NTX holds
b₁ is closed ;

end;

registration

let NTX be NTopSpace;

cluster non empty closed for Element of bool the carrier of NTX;

existence
ex b₁ being Subset of NTX st
( not b₁ is empty & b₁ is closed )

proof end;

end;

definition

let S, T be non empty TopSpace;
let f be Function of S,T;

func Top2NTop f -> Function of (Top2NTop S),(Top2NTop T) equals :: FINTOPO8:def 10
f;

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

proof end;

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;

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;

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

correctness
coherence
Top2NTop f is continuous Function of (Top2NTop TX),(Top2NTop TY);
compatibility
for b₁ being continuous Function of (Top2NTop TX),(Top2NTop TY) holds
( b₁ = Top2NTop f iff b₁ = f );

proof end;

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;

definition

let NT be NTopSpace;

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 ;

end;

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

registration

cluster non empty strict U_FMT_filter U_FMT_with_point U_FMT_local T_2 for FMT_Space_Str ;

existence
ex b₁ being NTopSpace st b₁ is T_2

proof end;

end;

definition

let NT be NTopSpace;

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;

end;

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

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

let NT be NTopSpace;
let x be Point of NT;

func NTop2Top x -> Point of (NTop2Top NT) equals :: FINTOPO8:def 14
x;

coherence
x is Point of (NTop2Top NT) by FINTOPO7:def 16;

end;

:: deftheorem defines NTop2Top FINTOPO8:def 14 :
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;

func Top2NTop x -> Point of (Top2NTop T) equals :: FINTOPO8:def 15
x;

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

end;

:: deftheorem defines Top2NTop FINTOPO8:def 15 :
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;

func NTop2Top S -> Subset of (NTop2Top NT) equals :: FINTOPO8:def 16
S;

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

end;

:: deftheorem defines NTop2Top FINTOPO8:def 16 :
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;

func Top2NTop S -> Subset of (Top2NTop T) equals :: FINTOPO8:def 17
S;

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

end;

:: deftheorem defines Top2NTop FINTOPO8:def 17 :
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

cluster non empty strict U_FMT_filter U_FMT_with_point U_FMT_local normal for FMT_Space_Str ;

existence
ex b₁ being NTopSpace st
( not b₁ is empty & b₁ is normal )

proof end;

end;

definition

let TX, TY be NTopSpace;
let f be Function of TX,TY;

func NTop2Top f -> Function of (NTop2Top TX),(NTop2Top TY) equals :: FINTOPO8:def 18
f;

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

proof end;

end;

:: deftheorem defines NTop2Top FINTOPO8:def 18 :
for TX, TY being NTopSpace
for f being Function of TX,TY holds NTop2Top f = f;

definition

func FMT_R^1 -> NTopSpace equals :: FINTOPO8:def 19
Top2NTop R^1;

coherence
Top2NTop R^1 is NTopSpace ;

end;

:: deftheorem defines FMT_R^1 FINTOPO8:def 19 :
FMT_R^1 = Top2NTop R^1;

theorem :: FINTOPO8:2

the carrier of FMT_R^1 = REAL by TOPMETR:17, FINTOPO7:def 15;

registration

cluster FMT_R^1 -> real-membered ;

coherence
FMT_R^1 is real-membered

proof end;

end;

theorem :: FINTOPO8:3

for NT being NTopSpace
for O being open Subset of NT holds O is open Subset of (NTop2Top NT) by Lm9;

theorem :: FINTOPO8:4

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

theorem :: FINTOPO8:5

for NT being NTopSpace holds
( [#] NT is open & {} NT is open ) ;

theorem :: FINTOPO8:6

for NT, NTY being NTopSpace
for y being Point of NTY holds NT --> y is continuous by Lm3;

theorem :: FINTOPO8:7

for NT being NTopSpace
for A being Subset of NT
for a being Point of NT holds
( a is_interior_point_of A iff ex O being open Subset of NT st
( a in O & O c= A ) ) by Lm4;

theorem :: FINTOPO8:8

for NT being NTopSpace
for O being open Subset of NT
for a being Point of NT st a in O holds
a is_interior_point_of O by Lm4;

theorem :: FINTOPO8:9

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 } by Lm5;

theorem :: FINTOPO8:10

for NT being NTopSpace
for A being Subset of NT holds Int A c= A by Lm15;

theorem :: FINTOPO8:11

for NT being NTopSpace
for A, B being Subset of NT st A c= B holds
Int A c= Int B by Lm17;

theorem Th12: :: FINTOPO8:12

for NT being NTopSpace
for A being Subset of NT holds
( A is open iff Int A = A )

proof end;

theorem :: FINTOPO8:13

for NT being NTopSpace
for A being Subset of NT holds Int A = Int (Int A) by Th12;

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

proof end;

theorem :: FINTOPO8:15

for NTX, NTY being NTopSpace
for x being Point of NTX
for f being Function of NTX,NTY holds filter_image (f,(U_FMT x)) = { M where M is Subset of NTY : f " M in U_FMT x } by CARDFIL2:def 13;

theorem :: FINTOPO8:16

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

theorem :: FINTOPO8:17

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

theorem :: FINTOPO8:18

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 holds
( f is_continuous_at x iff for V being Element of U_FMT y ex W being Element of U_FMT x st f .: W c= V ) by Lm11, Lm25;

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;

theorem :: FINTOPO8:20

for NTX, NTY being NTopSpace
for XA being Subset of NTX
for fc being continuous Function of NTX,NTY holds fc .: (Cl XA) c= Cl (fc .: XA) by Lm13;

theorem :: FINTOPO8:21

for NT being NTopSpace
for A being closed Subset of NT holds A is closed Subset of (NTop2Top NT) by Lm29;

theorem :: FINTOPO8:22

for NT being NTopSpace
for A, B being Subset of NT st B = ([#] NT) \ A holds
([#] NT) \ (Cl A) = Int B by Lm14;

theorem :: FINTOPO8:23

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

proof end;

theorem :: FINTOPO8:24

for NT being NTopSpace
for A being Subset of NT holds A c= Cl A by Lm21;

theorem :: FINTOPO8:25

for NT being NTopSpace
for A being Subset of NT holds
( A is closed iff Cl A = A ) by Lm20, Lm22;

theorem :: FINTOPO8:26

for NT being NTopSpace
for A, B being Subset of NT st A c= B holds
Cl A c= Cl B by Lm18;

theorem :: FINTOPO8:27

for NTX, NTY being NTopSpace
for f being Function of NTX,NTY st ( for XA being Subset of NTX holds f .: (Cl XA) c= Cl (f .: XA) ) holds
for S being closed Subset of NTY holds f " S is closed Subset of NTX by Lm23;

theorem :: FINTOPO8:28

for NT being NTopSpace
for A, B being Subset of NT st B = ([#] NT) \ A holds
( A is open iff B is closed ) by Lm6;

theorem :: FINTOPO8:29

for NT being NTopSpace
for A, B being Subset of NT st A = ([#] NT) \ B holds
( A is open iff B is closed ) ;

theorem :: FINTOPO8:30

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

theorem :: FINTOPO8:31

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

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 )

proof end;

theorem :: FINTOPO8:33

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 ) by Lm27;

theorem Th34: :: FINTOPO8:34

for NT being NTopSpace
for A being Subset of NT holds Int A = Int (NTop2Top A)

proof end;

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

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

proof end;

theorem :: FINTOPO8:37

for NT being NTopSpace
for A, B being Subset of NT st A misses B holds
NTop2Top A misses NTop2Top B ;

theorem :: FINTOPO8:38

for NT being NTopSpace
for A, B being Subset of NT st A misses B holds
Int A misses Int B

proof end;

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

proof end;

theorem :: FINTOPO8:40

for NT being T_2 NTopSpace holds NTop2Top NT is non empty strict T_2 TopSpace

proof end;

theorem Th41: :: FINTOPO8:41

for NT being normal NTopSpace holds NTop2Top NT is normal

proof end;

registration

let NT be normal NTopSpace;

cluster NTop2Top NT -> normal ;

coherence
NTop2Top NT is normal by Th41;

end;

theorem :: FINTOPO8:42

for T being non empty TopSpace
for A being Subset of T holds A is Subset of (Top2NTop T) by FINTOPO7:def 15;

theorem :: FINTOPO8:43

for T being non empty TopSpace
for F being closed Subset of T holds F is closed Subset of (Top2NTop T) by Lm7;

theorem :: FINTOPO8:44

for T being non empty TopSpace
for O being open Subset of T holds O is open Subset of (Top2NTop T) by Lm1;

theorem :: FINTOPO8:45

for T being non empty TopSpace
for A, B being Subset of T st A misses B holds
Top2NTop A misses Top2NTop B ;

theorem :: FINTOPO8:46

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

theorem :: FINTOPO8:47

for T being non empty strict TopSpace
for A being Subset of T holds Int A = Int (Top2NTop A) by Lm30;

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;

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

proof end;

theorem TH: :: FINTOPO8:50

for T being non empty strict normal TopSpace holds Top2NTop T is normal

proof end;

registration

let T be non empty strict normal TopSpace;

cluster Top2NTop T -> normal ;

coherence
Top2NTop T is normal by TH;

end;

theorem :: FINTOPO8:51

NTop2Top FMT_R^1 = R^1 by FINTOPO7:24;

theorem Th52: :: FINTOPO8:52

the carrier of FMT_R^1 = REAL by TOPMETR:17, FINTOPO7:def 15;

theorem :: FINTOPO8:53

for NT being NTopSpace
for f being Function of NT,FMT_R^1 holds NTop2Top f is Function of (NTop2Top NT),R^1 by FINTOPO7:24;

theorem :: FINTOPO8:54

for T being non empty TopSpace
for f being Function of T,R^1 holds Top2NTop f is Function of (Top2NTop T),(Top2NTop R^1) ;

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

proof end;

theorem :: FINTOPO8:56

{ ].a,b.[ where a, b is Real : a < b } is Basis of R^1 by TOPGEN_5:72;

theorem Th57: :: FINTOPO8:57

{ ].a,b.[ where a, b is Real : a < b } is Basis of FMT_R^1

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

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;

theorem :: FINTOPO8:60

for x being Point of FMT_R^1
for y being Point of RealSpace
for r being Real st x = y holds
Ball (y,r) = ].(x - r),(x + r).[ by FRECHET:7;

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

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;

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

proof end;

definition

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
ex b₁ 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₁ . r = Balls x )

proof end;

uniqueness
for b₁, b₂ 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₁ . r = Balls x ) ) & ( for r being Real ex x being Point of (TopSpaceMetr RealSpace) st
( x = r & b₂ . r = Balls x ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def20 defines gen_NS_R^1 FINTOPO8:def 20 :
for b₁ being Function of the carrier of FMT_R^1,(bool (bool the carrier of FMT_R^1)) holds
( b₁ = gen_NS_R^1 iff for r being Real ex x being Point of (TopSpaceMetr RealSpace) st
( x = r & b₁ . r = Balls x ) );

definition

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 #) is non empty strict FMT_Space_Str ;

end;

:: deftheorem defines gen_R^1 FINTOPO8:def 21 :
gen_R^1 = FMT_Space_Str(# the carrier of FMT_R^1,gen_NS_R^1 #);

theorem Th64: :: FINTOPO8:64

the carrier of gen_R^1 = REAL by FINTOPO7:def 15, TOPMETR:17;

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 )

proof end;

theorem :: FINTOPO8:66

dom <.gen_R^1.] = REAL by Th64, FUNCT_2:def 1;

theorem :: FINTOPO8:67

gen_filter gen_R^1 = FMT_R^1

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

proof end;