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