:: 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
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, SUBSET_1, FUNCT_1, RELAT_1, CARD_FIL, STRUCT_0,
PRE_TOPC, RCOMP_1, ORDINAL2, ZFMISC_1, PCOMPS_1, FINTOPO7, FUNCOP_1,
FINTOPO2, TARSKI, CARDFIL2, TOPS_1, TMAP_1, SETFAM_1, CONNSP_2, NATTRA_1,
TOPMETR, REAL_1, XXREAL_0, CARD_1, MEMBERED, XREAL_0, XXREAL_1, ARYTM_1,
ARYTM_3, RLVECT_3, CANTOR_1, NUMBERS, METRIC_1, FRECHET, FILTER_0, NAT_1,
FINTOPO8;
notations FUNCT_2, NUMBERS, SUBSET_1, TARSKI, FUNCT_1, RELSET_1, XBOOLE_0,
STRUCT_0, CARD_FIL, FINTOPO2, ZFMISC_1, PRE_TOPC, CARDFIL2, CONNSP_2,
TOPS_1, TDLAT_3, XREAL_0, TOPMETR, XXREAL_0, XCMPLX_0, RCOMP_1, TOPS_2,
CANTOR_1, FINTOPO7, METRIC_1, PCOMPS_1, ORDINAL1, FRECHET;
constructors CARDFIL2, FINTOPO7, TOPS_1, TDLAT_3, SUPINF_2, TOPMETR, FUNCOP_1,
RCOMP_1, TOPS_2, CANTOR_1, FRECHET, YELLOW_8;
registrations MEMBERED, TOPMETR, VALUED_0, YELLOW13, STRUCT_0, PRE_TOPC,
TOPS_1, FINTOPO7, SUBSET_1, RELSET_1, FUNCT_2, TEX_1, XREAL_0, CANTOR_1,
METRIC_1, PCOMPS_1, ORDINAL1, FRECHET, ZFMISC_1;
requirements ARITHM, NUMERALS, SUBSET, BOOLE, REAL;
begin :: Some trivial results in TopSpace
reserve T for TopSpace,
A,B for Subset of T;
theorem :: FINTOPO8:1
A misses B implies Int A misses Int B;
begin :: Some redefinitions: NTopSpace
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;
begin
registration
let NTX be non empty NTopSpace;
cluster [#] NTX -> open;
cluster {} NTX -> open;
end;
definition
let NTX be U_FMT_filter non empty strict FMT_Space_Str;
let x be Element of NTX;
redefine func U_FMT x -> Filter of the carrier of NTX;
end;
definition
let NTX be U_FMT_filter non empty strict 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};
end;
definition
let NTX,NTY be U_FMT_filter non empty strict FMT_Space_Str,
f be Function of NTX,NTY,
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);
end;
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;
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 be Element of U_FMT x holds V meets A;
end;
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};
end;
definition
let NTX,NTY be NTopSpace,
f be Function of NTX,NTY,
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;
definition
let NTX,NTY be NTopSpace,
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;
registration
let NTX,NTY be NTopSpace;
cluster continuous for Function of NTX,NTY;
end;
registration
let NT be NTopSpace;
let A be Subset of NT;
cluster Int A -> open;
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};
end;
definition
let NTX be NTopSpace;
let A be Subset of NTX;
attr A is closed means
:: FINTOPO8:def 9
([#] NTX) \ A is open Subset of NTX;
end;
registration
let NTX be NTopSpace;
cluster closed for Subset of NTX;
end;
registration
let NTX be NTopSpace;
cluster [#] NTX -> closed for Subset of NTX;
cluster {} NTX -> closed for Subset of NTX;
end;
registration
let NTX be NTopSpace;
cluster non empty closed for Subset of NTX;
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;
end;
definition
let TX being non empty TopSpace,
TY being non empty strict TopSpace;
let f be continuous Function of TX,TY;
redefine func Top2NTop f ->
continuous Function of Top2NTop TX,Top2NTop TY equals
:: FINTOPO8:def 11
f;
end;
definition
let NT be NTopSpace;
attr NT is T_2 means
:: FINTOPO8:def 12
for F being Filter of the carrier of NT holds
lim_filter F is trivial;
end;
registration
cluster T_2 for NTopSpace;
end;
definition
let NT be NTopSpace;
attr NT is normal means
:: FINTOPO8:def 13
for A,B being closed Subset of NT st A misses B holds
ex V being a_neighborhood of A,
W being a_neighborhood of B st V misses W;
end;
definition
let NT be NTopSpace;
let x be Point of NT;
func NTop2Top x -> Point of NTop2Top NT equals
:: FINTOPO8:def 14
x;
end;
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;
end;
definition
let NT be NTopSpace;
let S be Subset of NT;
func NTop2Top S -> Subset of NTop2Top NT equals
:: FINTOPO8:def 16
S;
end;
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;
end;
registration
cluster non empty normal for NTopSpace;
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;
end;
definition
func FMT_R^1 -> NTopSpace equals
:: FINTOPO8:def 19
Top2NTop R^1;
end;
theorem :: FINTOPO8:2
the carrier of FMT_R^1 = REAL;
registration
cluster FMT_R^1 -> real-membered;
end;
begin :: Some properties of NTopSpace
reserve NT,NTX,NTY for NTopSpace,
A,B for Subset of NT,
O for open Subset of NT,
a for Point of NT,
XA for Subset of NTX,
YB for Subset of NTY,
x for Point of NTX,
y for Point of NTY,
f for Function of NTX,NTY,
fc for continuous Function of NTX,NTY;
theorem :: FINTOPO8:3
O is open Subset of NTop2Top NT;
theorem :: FINTOPO8:4
A is Subset of NTop2Top NT;
theorem :: FINTOPO8:5
[#]NT is open & {} NT is open;
theorem :: FINTOPO8:6
NT --> y is continuous;
theorem :: FINTOPO8:7
(a is_interior_point_of A iff
ex O be open Subset of NT st a in O & O c= A);
theorem :: FINTOPO8:8
a in O implies a is_interior_point_of O;
theorem :: FINTOPO8:9
Int A = union {O where O is open Subset of NT: O c= A};
theorem :: FINTOPO8:10
Int A c= A;
theorem :: FINTOPO8:11
A c= B implies Int A c= Int B;
theorem :: FINTOPO8:12
A is open iff Int A = A;
theorem :: FINTOPO8:13
Int A = Int Int A;
theorem :: FINTOPO8:14
for NT be non empty strict NTopSpace
for A be Subset of NT
for x be Point of NT st
A is a_neighborhood of x holds Int A is open a_neighborhood of x;
theorem :: FINTOPO8:15
filter_image(f,U_FMT x) =
{M where M is Subset of NTY: f"(M) in U_FMT x};
theorem :: FINTOPO8:16
(f is_continuous_at x & y = f.x) implies
(for V being Element of U_FMT y ex W being Element of U_FMT x st f.:W c= V);
theorem :: FINTOPO8:17
y = f.x &
(for V being Element of U_FMT y ex W being Element of U_FMT x st f.:W c= V)
implies f is_continuous_at x;
theorem :: FINTOPO8:18
y = f.x implies
(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));
theorem :: FINTOPO8:19
(f is_continuous_at x &
x is_adherent_point_of XA & y = f.x & YB = f.:XA) implies
y is_adherent_point_of YB;
theorem :: FINTOPO8:20
fc.:(Cl XA) c= Cl(fc.:XA);
theorem :: FINTOPO8:21
for A being closed Subset of NT holds A is closed Subset of NTop2Top NT;
theorem :: FINTOPO8:22
B = [#] NT \ A implies [#] NT \ Cl A = Int B;
theorem :: FINTOPO8:23
B = [#] NT \ A implies [#] NT \ Int A = Cl B;
theorem :: FINTOPO8:24
A c= Cl A;
theorem :: FINTOPO8:25
A is closed iff Cl A = A;
theorem :: FINTOPO8:26
A c= B implies Cl A c= Cl B;
theorem :: FINTOPO8:27
(for XA being Subset of NTX holds f.:(Cl XA) c= Cl(f.:XA)) implies
(for S being closed Subset of NTY holds f"S is closed Subset of NTX);
theorem :: FINTOPO8:28
B = [#]NT \ A implies (A is open iff B is closed);
theorem :: FINTOPO8:29
A = [#]NT \ B implies (A is open iff B is closed);
theorem :: FINTOPO8:30
(for S being closed Subset of NTY holds f"S is closed Subset of NTX)
implies
(for S being open Subset of NTY holds f"S is open Subset of NTX);
theorem :: FINTOPO8:31
(for S being open Subset of NTY holds f"S is open Subset of NTX)
implies f is continuous;
theorem :: FINTOPO8:32
f is continuous iff for O being open Subset of NTY holds
f"O is open Subset of NTX;
theorem :: FINTOPO8:33
f is continuous iff for O being closed Subset of NTY holds
f"O is closed Subset of NTX;
theorem :: FINTOPO8:34
Int A = Int NTop2Top A;
theorem :: FINTOPO8:35
A is a_neighborhood of a implies NTop2Top A is a_neighborhood of NTop2Top a;
theorem :: FINTOPO8:36
A is a_neighborhood of B implies
NTop2Top A is a_neighborhood of NTop2Top B;
theorem :: FINTOPO8:37
A misses B implies NTop2Top A misses NTop2Top B;
theorem :: FINTOPO8:38
A misses B implies Int A misses Int B;
reserve NT for T_2 NTopSpace;
theorem :: FINTOPO8:39
for x,y being Point of NT st x <> y ex Vx being Element of U_FMT x,
Vy being Element of U_FMT y st Vx misses Vy;
theorem :: FINTOPO8:40
NTop2Top NT is T_2 non empty strict TopSpace;
theorem :: FINTOPO8:41
for NT being non empty normal NTopSpace holds NTop2Top NT is normal;
registration
let NT be non empty normal NTopSpace;
cluster NTop2Top NT -> normal;
end;
begin :: Some properties between TopSpace and NTopSpace
reserve T for non empty TopSpace,
A,B for Subset of T,
F for closed Subset of T,
O for open Subset of T;
theorem :: FINTOPO8:42
A is Subset of Top2NTop T;
theorem :: FINTOPO8:43
F is closed Subset of Top2NTop T;
theorem :: FINTOPO8:44
O is open Subset of Top2NTop T;
theorem :: FINTOPO8:45
A misses B implies Top2NTop A misses Top2NTop B;
theorem :: FINTOPO8:46
for T being T_2 non empty TopSpace holds Top2NTop T is T_2 NTopSpace;
reserve T for non empty strict TopSpace,
A,B for Subset of T,
x for Point of T;
theorem :: FINTOPO8:47
Int A = Int Top2NTop A;
theorem :: FINTOPO8:48
A is a_neighborhood of B implies Top2NTop A is a_neighborhood of Top2NTop B;
theorem :: FINTOPO8:49
A is a_neighborhood of x implies Top2NTop A is a_neighborhood of Top2NTop x;
theorem :: FINTOPO8:50
for T being non empty normal strict TopSpace holds Top2NTop T is normal;
registration
let T be non empty normal strict TopSpace;
cluster Top2NTop T -> normal;
end;
begin :: Transport from R^1 to FMT_R^1
reserve A for Subset of FMT_R^1,
x for Point of FMT_R^1,
y for Point of RealSpace,
z for Point of TopSpaceMetr RealSpace,
r for Real;
theorem :: FINTOPO8:51
NTop2Top FMT_R^1 = R^1;
theorem :: FINTOPO8:52
the carrier of FMT_R^1 = REAL;
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;
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 :: FINTOPO8:55
A is open iff for x being Real st x in A
ex r st r > 0 & ].x - r, x + r.[ c= A;
theorem :: FINTOPO8:56
{].a,b.[ where a,b is Real: a < b} is Basis of R^1;
theorem :: FINTOPO8:57
{].a,b.[ where a,b is Real: a < b} is Basis of FMT_R^1;
theorem :: FINTOPO8:58
r > 0 implies ].x - r , x + r.[ is a_neighborhood of x;
theorem :: FINTOPO8:59
for x being object holds x is Point of FMT_R^1 iff x is Point of RealSpace;
theorem :: FINTOPO8:60
x = y implies Ball(y,r) = ]. x - r , x + r .[;
theorem :: FINTOPO8:61
x = y & r > 0 implies Ball(y,r) is a_neighborhood of x;
theorem :: FINTOPO8:62
x = z implies Balls(z) is Subset-Family of FMT_R^1;
theorem :: FINTOPO8:63
for SF being Subset-Family of FMT_R^1
st x = z & SF = Balls(z)
holds <. SF .] = U_FMT x;
definition
func gen_NS_R^1 -> Function of the carrier of
FMT_R^1,bool bool the carrier of FMT_R^1 means
:: FINTOPO8:def 20
for r being Real holds ex x being Point of TopSpaceMetr(RealSpace)
st x = r & it.r = Balls(x);
end;
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 #);
end;
theorem :: FINTOPO8:64
the carrier of gen_R^1 = REAL;
theorem :: FINTOPO8:65
for x being Element of gen_R^1 holds
ex y being Point of TopSpaceMetr(RealSpace) st x = y &
U_FMT x = Balls(y);
theorem :: FINTOPO8:66
dom <. gen_R^1 .] = REAL;
theorem :: FINTOPO8:67
gen_filter(gen_R^1) = FMT_R^1;
begin :: Transport Urysohn's lemma (URYSOHN3:20) from TopSpace to NTopSpace
theorem :: FINTOPO8:68
for NT being non empty normal NTopSpace, 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);