:: Urysohn Lemma :: by J\'ozef Bia{\l}as and Yatsuka Nakamura :: :: Received February 16, 2001 :: Copyright (c) 2001-2012 Association of Mizar Users begin Lm1: for T being non empty normal TopSpace for A, B being closed Subset of T st A <> {} & A misses B holds ex G being Function of (dyadic 0),(bool the carrier of T) st ( A c= G . 0 & B = ([#] T) \ (G . 1) & ( for r1, r2 being Element of dyadic 0 st r1 < r2 holds ( G . r1 is open & G . r2 is open & Cl (G . r1) c= G . r2 ) ) ) proofend; theorem Th1: :: URYSOHN3:1 for T being non empty normal TopSpace for A, B being closed Subset of T st A <> {} & A misses B holds for n being Element of NAT ex G being Function of (dyadic n),(bool the carrier of T) st ( A c= G . 0 & B = ([#] T) \ (G . 1) & ( for r1, r2 being Element of dyadic n st r1 < r2 holds ( G . r1 is open & G . r2 is open & Cl (G . r1) c= G . r2 ) ) ) proofend; definition let T be non empty TopSpace; let A, B be Subset of T; let n be Element of NAT ; assume A1: ( T is normal & A <> {} & A is closed & B is closed & A misses B ) ; mode Drizzle of A,B,n -> Function of (dyadic n),(bool the carrier of T) means :Def1: :: URYSOHN3:def 1 ( A c= it . 0 & B = ([#] T) \ (it . 1) & ( for r1, r2 being Element of dyadic n st r1 < r2 holds ( it . r1 is open & it . r2 is open & Cl (it . r1) c= it . r2 ) ) ); existence ex b1 being Function of (dyadic n),(bool the carrier of T) st ( A c= b1 . 0 & B = ([#] T) \ (b1 . 1) & ( for r1, r2 being Element of dyadic n st r1 < r2 holds ( b1 . r1 is open & b1 . r2 is open & Cl (b1 . r1) c= b1 . r2 ) ) ) by A1, Th1; end; :: deftheorem Def1 defines Drizzle URYSOHN3:def_1_:_ for T being non empty TopSpace for A, B being Subset of T for n being Element of NAT st T is normal & A <> {} & A is closed & B is closed & A misses B holds for b5 being Function of (dyadic n),(bool the carrier of T) holds ( b5 is Drizzle of A,B,n iff ( A c= b5 . 0 & B = ([#] T) \ (b5 . 1) & ( for r1, r2 being Element of dyadic n st r1 < r2 holds ( b5 . r1 is open & b5 . r2 is open & Cl (b5 . r1) c= b5 . r2 ) ) ) ); theorem Th2: :: URYSOHN3:2 for T being non empty normal TopSpace for A, B being closed Subset of T st A <> {} & A misses B holds for n being Element of NAT for G being Drizzle of A,B,n ex F being Drizzle of A,B,n + 1 st for r being Element of dyadic (n + 1) st r in dyadic n holds F . r = G . r proofend; theorem Th3: :: URYSOHN3:3 for T being non empty TopSpace for A, B being Subset of T for n being Element of NAT for S being Drizzle of A,B,n holds S is Element of PFuncs (DYADIC,(bool the carrier of T)) proofend; definition let A, B be non empty set ; let F be Function of NAT,(PFuncs (A,B)); let n be Element of NAT ; :: original:. redefine funcF . n -> Element of PFuncs (A,B); coherence F . n is Element of PFuncs (A,B) by FUNCT_2:5; end; theorem Th4: :: URYSOHN3:4 for T being non empty normal TopSpace for A, B being closed Subset of T st A <> {} & A misses B holds ex F being Functional_Sequence of DYADIC,(bool the carrier of T) st for n being Element of NAT holds ( F . n is Drizzle of A,B,n & ( for r being Element of dom (F . n) holds (F . n) . r = (F . (n + 1)) . r ) ) proofend; definition let T be non empty TopSpace; let A, B be Subset of T; assume A1: ( T is normal & A <> {} & A is closed & B is closed & A misses B ) ; mode Rain of A,B -> Functional_Sequence of DYADIC,(bool the carrier of T) means :Def2: :: URYSOHN3:def 2 for n being Element of NAT holds ( it . n is Drizzle of A,B,n & ( for r being Element of dom (it . n) holds (it . n) . r = (it . (n + 1)) . r ) ); existence ex b1 being Functional_Sequence of DYADIC,(bool the carrier of T) st for n being Element of NAT holds ( b1 . n is Drizzle of A,B,n & ( for r being Element of dom (b1 . n) holds (b1 . n) . r = (b1 . (n + 1)) . r ) ) by A1, Th4; end; :: deftheorem Def2 defines Rain URYSOHN3:def_2_:_ for T being non empty TopSpace for A, B being Subset of T st T is normal & A <> {} & A is closed & B is closed & A misses B holds for b4 being Functional_Sequence of DYADIC,(bool the carrier of T) holds ( b4 is Rain of A,B iff for n being Element of NAT holds ( b4 . n is Drizzle of A,B,n & ( for r being Element of dom (b4 . n) holds (b4 . n) . r = (b4 . (n + 1)) . r ) ) ); definition let x be Real; assume A1: x in DYADIC ; func inf_number_dyadic x -> Element of NAT means :Def3: :: URYSOHN3:def 3 ( ( x in dyadic 0 implies it = 0 ) & ( it = 0 implies x in dyadic 0 ) & ( for n being Element of NAT st x in dyadic (n + 1) & not x in dyadic n holds it = n + 1 ) ); existence ex b1 being Element of NAT st ( ( x in dyadic 0 implies b1 = 0 ) & ( b1 = 0 implies x in dyadic 0 ) & ( for n being Element of NAT st x in dyadic (n + 1) & not x in dyadic n holds b1 = n + 1 ) ) proofend; uniqueness for b1, b2 being Element of NAT holds not ( ( x in dyadic 0 implies b1 = 0 ) & ( b1 = 0 implies x in dyadic 0 ) & ( for n being Element of NAT st x in dyadic (n + 1) & not x in dyadic n holds b1 = n + 1 ) & ( x in dyadic 0 implies b2 = 0 ) & ( b2 = 0 implies x in dyadic 0 ) & ( for n being Element of NAT st x in dyadic (n + 1) & not x in dyadic n holds b2 = n + 1 ) & not b1 = b2 ) proofend; end; :: deftheorem Def3 defines inf_number_dyadic URYSOHN3:def_3_:_ for x being Real st x in DYADIC holds for b2 being Element of NAT holds ( b2 = inf_number_dyadic x iff ( ( x in dyadic 0 implies b2 = 0 ) & ( b2 = 0 implies x in dyadic 0 ) & ( for n being Element of NAT st x in dyadic (n + 1) & not x in dyadic n holds b2 = n + 1 ) ) ); theorem Th5: :: URYSOHN3:5 for x being Real st x in DYADIC holds x in dyadic (inf_number_dyadic x) proofend; theorem Th6: :: URYSOHN3:6 for x being Real st x in DYADIC holds for n being Element of NAT st inf_number_dyadic x <= n holds x in dyadic n proofend; theorem Th7: :: URYSOHN3:7 for x being Real for n being Element of NAT st x in dyadic n holds inf_number_dyadic x <= n proofend; theorem Th8: :: URYSOHN3:8 for T being non empty normal TopSpace for A, B being closed Subset of T st A <> {} & A misses B holds for G being Rain of A,B for x being Real st x in DYADIC holds for n being Element of NAT holds (G . (inf_number_dyadic x)) . x = (G . ((inf_number_dyadic x) + n)) . x proofend; theorem Th9: :: URYSOHN3:9 for T being non empty normal TopSpace for A, B being closed Subset of T st A <> {} & A misses B holds for G being Rain of A,B for x being Real st x in DYADIC holds ex y being Subset of T st for n being Element of NAT st x in dyadic n holds y = (G . n) . x proofend; theorem Th10: :: URYSOHN3:10 for T being non empty normal TopSpace for A, B being closed Subset of T st A <> {} & A misses B holds for G being Rain of A,B ex F being Function of DOM,(bool the carrier of T) st for x being Real st x in DOM holds ( ( x in halfline 0 implies F . x = {} ) & ( x in right_open_halfline 1 implies F . x = the carrier of T ) & ( x in DYADIC implies for n being Element of NAT st x in dyadic n holds F . x = (G . n) . x ) ) proofend; definition let T be non empty TopSpace; let A, B be Subset of T; assume A1: ( T is normal & A <> {} & A is closed & B is closed & A misses B ) ; let R be Rain of A,B; func Tempest R -> Function of DOM,(bool the carrier of T) means :Def4: :: URYSOHN3:def 4 for x being Real st x in DOM holds ( ( x in halfline 0 implies it . x = {} ) & ( x in right_open_halfline 1 implies it . x = the carrier of T ) & ( x in DYADIC implies for n being Element of NAT st x in dyadic n holds it . x = (R . n) . x ) ); existence ex b1 being Function of DOM,(bool the carrier of T) st for x being Real st x in DOM holds ( ( x in halfline 0 implies b1 . x = {} ) & ( x in right_open_halfline 1 implies b1 . x = the carrier of T ) & ( x in DYADIC implies for n being Element of NAT st x in dyadic n holds b1 . x = (R . n) . x ) ) by A1, Th10; uniqueness for b1, b2 being Function of DOM,(bool the carrier of T) st ( for x being Real st x in DOM holds ( ( x in halfline 0 implies b1 . x = {} ) & ( x in right_open_halfline 1 implies b1 . x = the carrier of T ) & ( x in DYADIC implies for n being Element of NAT st x in dyadic n holds b1 . x = (R . n) . x ) ) ) & ( for x being Real st x in DOM holds ( ( x in halfline 0 implies b2 . x = {} ) & ( x in right_open_halfline 1 implies b2 . x = the carrier of T ) & ( x in DYADIC implies for n being Element of NAT st x in dyadic n holds b2 . x = (R . n) . x ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def4 defines Tempest URYSOHN3:def_4_:_ for T being non empty TopSpace for A, B being Subset of T st T is normal & A <> {} & A is closed & B is closed & A misses B holds for R being Rain of A,B for b5 being Function of DOM,(bool the carrier of T) holds ( b5 = Tempest R iff for x being Real st x in DOM holds ( ( x in halfline 0 implies b5 . x = {} ) & ( x in right_open_halfline 1 implies b5 . x = the carrier of T ) & ( x in DYADIC implies for n being Element of NAT st x in dyadic n holds b5 . x = (R . n) . x ) ) ); definition let X be non empty set ; let T be TopSpace; let F be Function of X,(bool the carrier of T); let x be Element of X; :: original:. redefine funcF . x -> Subset of T; correctness coherence F . x is Subset of T; proofend; end; theorem Th11: :: URYSOHN3:11 for T being non empty normal TopSpace for A, B being closed Subset of T st A <> {} & A misses B holds for G being Rain of A,B for r being Real for C being Subset of T st C = (Tempest G) . r & r in DOM holds C is open proofend; theorem Th12: :: URYSOHN3:12 for T being non empty normal TopSpace for A, B being closed Subset of T st A <> {} & A misses B holds for G being Rain of A,B for r1, r2 being Real st r1 in DOM & r2 in DOM & r1 < r2 holds for C being Subset of T st C = (Tempest G) . r1 holds Cl C c= (Tempest G) . r2 proofend; definition let T be non empty TopSpace; let A, B be Subset of T; let G be Rain of A,B; let p be Point of T; func Rainbow (p,G) -> Subset of ExtREAL means :Def5: :: URYSOHN3:def 5 for x being set holds ( x in it iff ( x in DYADIC & ( for s being Real st s = x holds not p in (Tempest G) . s ) ) ); existence ex b1 being Subset of ExtREAL st for x being set holds ( x in b1 iff ( x in DYADIC & ( for s being Real st s = x holds not p in (Tempest G) . s ) ) ) proofend; uniqueness for b1, b2 being Subset of ExtREAL st ( for x being set holds ( x in b1 iff ( x in DYADIC & ( for s being Real st s = x holds not p in (Tempest G) . s ) ) ) ) & ( for x being set holds ( x in b2 iff ( x in DYADIC & ( for s being Real st s = x holds not p in (Tempest G) . s ) ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def5 defines Rainbow URYSOHN3:def_5_:_ for T being non empty TopSpace for A, B being Subset of T for G being Rain of A,B for p being Point of T for b6 being Subset of ExtREAL holds ( b6 = Rainbow (p,G) iff for x being set holds ( x in b6 iff ( x in DYADIC & ( for s being Real st s = x holds not p in (Tempest G) . s ) ) ) ); theorem Th13: :: URYSOHN3:13 for T being non empty TopSpace for A, B being Subset of T for G being Rain of A,B for p being Point of T holds Rainbow (p,G) c= DYADIC proofend; definition let T be non empty TopSpace; let A, B be Subset of T; let R be Rain of A,B; func Thunder R -> Function of T,R^1 means :Def6: :: URYSOHN3:def 6 for p being Point of T holds ( ( Rainbow (p,R) = {} implies it . p = 0 ) & ( for S being non empty Subset of ExtREAL st S = Rainbow (p,R) holds it . p = sup S ) ); existence ex b1 being Function of T,R^1 st for p being Point of T holds ( ( Rainbow (p,R) = {} implies b1 . p = 0 ) & ( for S being non empty Subset of ExtREAL st S = Rainbow (p,R) holds b1 . p = sup S ) ) proofend; uniqueness for b1, b2 being Function of T,R^1 st ( for p being Point of T holds ( ( Rainbow (p,R) = {} implies b1 . p = 0 ) & ( for S being non empty Subset of ExtREAL st S = Rainbow (p,R) holds b1 . p = sup S ) ) ) & ( for p being Point of T holds ( ( Rainbow (p,R) = {} implies b2 . p = 0 ) & ( for S being non empty Subset of ExtREAL st S = Rainbow (p,R) holds b2 . p = sup S ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def6 defines Thunder URYSOHN3:def_6_:_ for T being non empty TopSpace for A, B being Subset of T for R being Rain of A,B for b5 being Function of T,R^1 holds ( b5 = Thunder R iff for p being Point of T holds ( ( Rainbow (p,R) = {} implies b5 . p = 0 ) & ( for S being non empty Subset of ExtREAL st S = Rainbow (p,R) holds b5 . p = sup S ) ) ); theorem Th14: :: URYSOHN3:14 for T being non empty TopSpace for A, B being Subset of T for G being Rain of A,B for p being Point of T for S being non empty Subset of ExtREAL st S = Rainbow (p,G) holds for e1 being R_eal st e1 = 1 holds ( 0. <= sup S & sup S <= e1 ) proofend; theorem Th15: :: URYSOHN3:15 for T being non empty normal TopSpace for A, B being closed Subset of T st A <> {} & A misses B holds for G being Rain of A,B for r being Element of DOM for p being Point of T st (Thunder G) . p < r holds p in (Tempest G) . r proofend; theorem Th16: :: URYSOHN3:16 for T being non empty normal TopSpace for A, B being closed Subset of T st A <> {} & A misses B holds for G being Rain of A,B for r being Real st r in DYADIC \/ (right_open_halfline 1) & 0 < r holds for p being Point of T st p in (Tempest G) . r holds (Thunder G) . p <= r proofend; theorem Th17: :: URYSOHN3:17 for T being non empty normal TopSpace for A, B being closed Subset of T st A <> {} & A misses B holds for G being Rain of A,B for r1 being Element of DOM st 0 < r1 holds for p being Point of T st r1 < (Thunder G) . p holds not p in (Tempest G) . r1 proofend; theorem Th18: :: URYSOHN3:18 for T being non empty normal TopSpace for A, B being closed Subset of T st A <> {} & A misses B holds for G being Rain of A,B holds ( Thunder G is continuous & ( for x being Point of T holds ( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) ) ) ) proofend; theorem Th19: :: URYSOHN3:19 for T being non empty normal TopSpace for A, B being closed Subset of T st A <> {} & A misses B holds ex F being Function of T,R^1 st ( F is continuous & ( for x being Point of T holds ( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) ) proofend; :: [WP: ] Urysohn_Lemma theorem Th20: :: URYSOHN3:20 for T being non empty normal TopSpace for A, B being closed Subset of T st A misses B holds ex F being Function of T,R^1 st ( F is continuous & ( for x being Point of T holds ( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) ) proofend; theorem :: URYSOHN3:21 for T being non empty T_2 compact TopSpace for A, B being closed Subset of T st A misses B holds ex F being Function of T,R^1 st ( F is continuous & ( for x being Point of T holds ( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) ) by Th20;