:: URYSOHN1 semantic presentation begin definition let n be Nat; func dyadic n -> Subset of REAL means :Def1: :: URYSOHN1:def 1 for x being Real holds ( x in it iff ex i being Element of NAT st ( i <= 2 |^ n & x = i / (2 |^ n) ) ); existence ex b1 being Subset of REAL st for x being Real holds ( x in b1 iff ex i being Element of NAT st ( i <= 2 |^ n & x = i / (2 |^ n) ) ) proof defpred S1[ set ] means ex i being Element of NAT st ( i <= 2 |^ n & $1 = i / (2 |^ n) ); ex X being Subset of REAL st for x being Real holds ( x in X iff S1[x] ) from SUBSET_1:sch_3(); hence ex b1 being Subset of REAL st for x being Real holds ( x in b1 iff ex i being Element of NAT st ( i <= 2 |^ n & x = i / (2 |^ n) ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Subset of REAL st ( for x being Real holds ( x in b1 iff ex i being Element of NAT st ( i <= 2 |^ n & x = i / (2 |^ n) ) ) ) & ( for x being Real holds ( x in b2 iff ex i being Element of NAT st ( i <= 2 |^ n & x = i / (2 |^ n) ) ) ) holds b1 = b2 proof let A1, A2 be Subset of REAL; ::_thesis: ( ( for x being Real holds ( x in A1 iff ex i being Element of NAT st ( i <= 2 |^ n & x = i / (2 |^ n) ) ) ) & ( for x being Real holds ( x in A2 iff ex i being Element of NAT st ( i <= 2 |^ n & x = i / (2 |^ n) ) ) ) implies A1 = A2 ) assume that A1: for x being Real holds ( x in A1 iff ex i being Element of NAT st ( i <= 2 |^ n & x = i / (2 |^ n) ) ) and A2: for x being Real holds ( x in A2 iff ex i being Element of NAT st ( i <= 2 |^ n & x = i / (2 |^ n) ) ) ; ::_thesis: A1 = A2 for a being set holds ( a in A1 iff a in A2 ) proof let a be set ; ::_thesis: ( a in A1 iff a in A2 ) thus ( a in A1 implies a in A2 ) ::_thesis: ( a in A2 implies a in A1 ) proof assume A3: a in A1 ; ::_thesis: a in A2 then reconsider a = a as Real ; ex i being Element of NAT st ( i <= 2 |^ n & a = i / (2 |^ n) ) by A1, A3; hence a in A2 by A2; ::_thesis: verum end; assume A4: a in A2 ; ::_thesis: a in A1 then reconsider a = a as Real ; ex i being Element of NAT st ( i <= 2 |^ n & a = i / (2 |^ n) ) by A2, A4; hence a in A1 by A1; ::_thesis: verum end; hence A1 = A2 by TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def1 defines dyadic URYSOHN1:def_1_:_ for n being Nat for b2 being Subset of REAL holds ( b2 = dyadic n iff for x being Real holds ( x in b2 iff ex i being Element of NAT st ( i <= 2 |^ n & x = i / (2 |^ n) ) ) ); definition func DYADIC -> Subset of REAL means :Def2: :: URYSOHN1:def 2 for a being Real holds ( a in it iff ex n being Element of NAT st a in dyadic n ); existence ex b1 being Subset of REAL st for a being Real holds ( a in b1 iff ex n being Element of NAT st a in dyadic n ) proof defpred S1[ set ] means ex i being Element of NAT st $1 in dyadic i; ex X being Subset of REAL st for x being Real holds ( x in X iff S1[x] ) from SUBSET_1:sch_3(); hence ex b1 being Subset of REAL st for a being Real holds ( a in b1 iff ex n being Element of NAT st a in dyadic n ) ; ::_thesis: verum end; uniqueness for b1, b2 being Subset of REAL st ( for a being Real holds ( a in b1 iff ex n being Element of NAT st a in dyadic n ) ) & ( for a being Real holds ( a in b2 iff ex n being Element of NAT st a in dyadic n ) ) holds b1 = b2 proof let A1, A2 be Subset of REAL; ::_thesis: ( ( for a being Real holds ( a in A1 iff ex n being Element of NAT st a in dyadic n ) ) & ( for a being Real holds ( a in A2 iff ex n being Element of NAT st a in dyadic n ) ) implies A1 = A2 ) assume that A1: for x being Real holds ( x in A1 iff ex n being Element of NAT st x in dyadic n ) and A2: for x being Real holds ( x in A2 iff ex n being Element of NAT st x in dyadic n ) ; ::_thesis: A1 = A2 for a being set holds ( a in A1 iff a in A2 ) proof let a be set ; ::_thesis: ( a in A1 iff a in A2 ) thus ( a in A1 implies a in A2 ) ::_thesis: ( a in A2 implies a in A1 ) proof assume A3: a in A1 ; ::_thesis: a in A2 then reconsider a = a as Real ; ex n being Element of NAT st a in dyadic n by A1, A3; hence a in A2 by A2; ::_thesis: verum end; thus ( a in A2 implies a in A1 ) ::_thesis: verum proof assume A4: a in A2 ; ::_thesis: a in A1 then reconsider a = a as Real ; ex n being Element of NAT st a in dyadic n by A2, A4; hence a in A1 by A1; ::_thesis: verum end; end; hence A1 = A2 by TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def2 defines DYADIC URYSOHN1:def_2_:_ for b1 being Subset of REAL holds ( b1 = DYADIC iff for a being Real holds ( a in b1 iff ex n being Element of NAT st a in dyadic n ) ); definition func DOM -> Subset of REAL equals :: URYSOHN1:def 3 ((halfline 0) \/ DYADIC) \/ (right_open_halfline 1); coherence ((halfline 0) \/ DYADIC) \/ (right_open_halfline 1) is Subset of REAL ; end; :: deftheorem defines DOM URYSOHN1:def_3_:_ DOM = ((halfline 0) \/ DYADIC) \/ (right_open_halfline 1); definition let T be TopSpace; let A be non empty Subset of REAL; let F be Function of A,(bool the carrier of T); let r be Element of A; :: original: . redefine funcF . r -> Subset of T; coherence F . r is Subset of T proof F . r is Subset of T ; hence F . r is Subset of T ; ::_thesis: verum end; end; theorem Th1: :: URYSOHN1:1 for n being Element of NAT for x being Real st x in dyadic n holds ( 0 <= x & x <= 1 ) proof let n be Element of NAT ; ::_thesis: for x being Real st x in dyadic n holds ( 0 <= x & x <= 1 ) let x be Real; ::_thesis: ( x in dyadic n implies ( 0 <= x & x <= 1 ) ) assume x in dyadic n ; ::_thesis: ( 0 <= x & x <= 1 ) then consider i being Element of NAT such that A1: i <= 2 |^ n and A2: x = i / (2 |^ n) by Def1; 0 <= i by NAT_1:2; then ( 0 / (2 |^ n) <= i / (2 |^ n) & i / (2 |^ n) <= (2 |^ n) / (2 |^ n) ) by A1, XREAL_1:72; hence ( 0 <= x & x <= 1 ) by A2, XCMPLX_1:60; ::_thesis: verum end; theorem Th2: :: URYSOHN1:2 dyadic 0 = {0,1} proof A1: 2 |^ 0 = 1 by NEWTON:4; A2: for x being Real holds ( x in dyadic 0 iff ex i being Element of NAT st ( i <= 1 & x = i ) ) proof let x be Real; ::_thesis: ( x in dyadic 0 iff ex i being Element of NAT st ( i <= 1 & x = i ) ) A3: ( ex i being Element of NAT st ( i <= 1 & x = i ) implies x in dyadic 0 ) proof given i being Element of NAT such that A4: i <= 1 and A5: x = i ; ::_thesis: x in dyadic 0 x = i / 1 by A5; hence x in dyadic 0 by A1, A4, Def1; ::_thesis: verum end; ( x in dyadic 0 implies ex i being Element of NAT st ( i <= 1 & x = i ) ) proof assume x in dyadic 0 ; ::_thesis: ex i being Element of NAT st ( i <= 1 & x = i ) then ex i being Element of NAT st ( i <= 1 & x = i / 1 ) by A1, Def1; hence ex i being Element of NAT st ( i <= 1 & x = i ) ; ::_thesis: verum end; hence ( x in dyadic 0 iff ex i being Element of NAT st ( i <= 1 & x = i ) ) by A3; ::_thesis: verum end; for x being set holds ( x in dyadic 0 iff x in {0,1} ) proof let x be set ; ::_thesis: ( x in dyadic 0 iff x in {0,1} ) A6: ( x in dyadic 0 implies x in {0,1} ) proof assume A7: x in dyadic 0 ; ::_thesis: x in {0,1} then reconsider x = x as Real ; consider i being Element of NAT such that A8: i <= 1 and A9: x = i by A2, A7; A10: 0 <= i by NAT_1:2; i <= 0 + 1 by A8; then ( x = 0 or x = 1 ) by A10, A9, NAT_1:9; hence x in {0,1} by TARSKI:def_2; ::_thesis: verum end; ( x in {0,1} implies x in dyadic 0 ) proof assume x in {0,1} ; ::_thesis: x in dyadic 0 then ( x = 0 or x = 1 ) by TARSKI:def_2; hence x in dyadic 0 by A2; ::_thesis: verum end; hence ( x in dyadic 0 iff x in {0,1} ) by A6; ::_thesis: verum end; hence dyadic 0 = {0,1} by TARSKI:1; ::_thesis: verum end; theorem :: URYSOHN1:3 dyadic 1 = {0,(1 / 2),1} proof A1: 2 |^ 1 = 2 by NEWTON:5; for x being set holds ( x in dyadic 1 iff x in {0,(1 / 2),1} ) proof let x be set ; ::_thesis: ( x in dyadic 1 iff x in {0,(1 / 2),1} ) A2: ( x in {0,(1 / 2),1} implies x in dyadic 1 ) proof assume A3: x in {0,(1 / 2),1} ; ::_thesis: x in dyadic 1 percases ( x = 0 or x = 1 / 2 or x = 1 ) by A3, ENUMSET1:def_1; suppose x = 0 ; ::_thesis: x in dyadic 1 then x = 0 / 2 ; hence x in dyadic 1 by A1, Def1; ::_thesis: verum end; suppose x = 1 / 2 ; ::_thesis: x in dyadic 1 hence x in dyadic 1 by A1, Def1; ::_thesis: verum end; supposeA4: x = 1 ; ::_thesis: x in dyadic 1 then reconsider x = x as Real ; x = 2 / 2 by A4; hence x in dyadic 1 by A1, Def1; ::_thesis: verum end; end; end; ( x in dyadic 1 implies x in {0,(1 / 2),1} ) proof assume A5: x in dyadic 1 ; ::_thesis: x in {0,(1 / 2),1} then reconsider x = x as Real ; consider i being Element of NAT such that A6: i <= 2 and A7: x = i / 2 by A1, A5, Def1; A8: 0 <= i by NAT_1:2; ( i <= 1 or i = 1 + 1 ) by A6, NAT_1:8; then ( i = 0 or i = 0 + 1 or i = 2 ) by A8, NAT_1:9; hence x in {0,(1 / 2),1} by A7, ENUMSET1:def_1; ::_thesis: verum end; hence ( x in dyadic 1 iff x in {0,(1 / 2),1} ) by A2; ::_thesis: verum end; hence dyadic 1 = {0,(1 / 2),1} by TARSKI:1; ::_thesis: verum end; registration let n be Nat; cluster dyadic n -> non empty ; coherence not dyadic n is empty proof set x = 0 / (2 |^ n); ex i being Element of NAT st ( 0 <= i & i <= 2 |^ n & 0 / (2 |^ n) = i / (2 |^ n) ) proof take 0 ; ::_thesis: ( 0 <= 0 & 0 <= 2 |^ n & 0 / (2 |^ n) = 0 / (2 |^ n) ) thus ( 0 <= 0 & 0 <= 2 |^ n & 0 / (2 |^ n) = 0 / (2 |^ n) ) by NEWTON:83; ::_thesis: verum end; hence not dyadic n is empty by Def1; ::_thesis: verum end; end; definition let n be Nat; func dyad n -> FinSequence means :Def4: :: URYSOHN1:def 4 ( dom it = Seg ((2 |^ n) + 1) & ( for i being Element of NAT st i in dom it holds it . i = (i - 1) / (2 |^ n) ) ); existence ex b1 being FinSequence st ( dom b1 = Seg ((2 |^ n) + 1) & ( for i being Element of NAT st i in dom b1 holds b1 . i = (i - 1) / (2 |^ n) ) ) proof deffunc H1( Nat) -> Element of REAL = ($1 - 1) / (2 |^ n); consider FS being FinSequence such that A1: ( len FS = (2 |^ n) + 1 & ( for i being Nat st i in dom FS holds FS . i = H1(i) ) ) from FINSEQ_1:sch_2(); take FS ; ::_thesis: ( dom FS = Seg ((2 |^ n) + 1) & ( for i being Element of NAT st i in dom FS holds FS . i = (i - 1) / (2 |^ n) ) ) thus ( dom FS = Seg ((2 |^ n) + 1) & ( for i being Element of NAT st i in dom FS holds FS . i = (i - 1) / (2 |^ n) ) ) by A1, FINSEQ_1:def_3; ::_thesis: verum end; uniqueness for b1, b2 being FinSequence st dom b1 = Seg ((2 |^ n) + 1) & ( for i being Element of NAT st i in dom b1 holds b1 . i = (i - 1) / (2 |^ n) ) & dom b2 = Seg ((2 |^ n) + 1) & ( for i being Element of NAT st i in dom b2 holds b2 . i = (i - 1) / (2 |^ n) ) holds b1 = b2 proof let F1, F2 be FinSequence; ::_thesis: ( dom F1 = Seg ((2 |^ n) + 1) & ( for i being Element of NAT st i in dom F1 holds F1 . i = (i - 1) / (2 |^ n) ) & dom F2 = Seg ((2 |^ n) + 1) & ( for i being Element of NAT st i in dom F2 holds F2 . i = (i - 1) / (2 |^ n) ) implies F1 = F2 ) assume that A2: dom F1 = Seg ((2 |^ n) + 1) and A3: for i being Element of NAT st i in dom F1 holds F1 . i = (i - 1) / (2 |^ n) and A4: dom F2 = Seg ((2 |^ n) + 1) and A5: for i being Element of NAT st i in dom F2 holds F2 . i = (i - 1) / (2 |^ n) ; ::_thesis: F1 = F2 consider X being set such that A6: X = dom F1 ; for k being Nat st k in X holds F1 . k = F2 . k proof let k be Nat; ::_thesis: ( k in X implies F1 . k = F2 . k ) assume A7: k in X ; ::_thesis: F1 . k = F2 . k hence F1 . k = (k - 1) / (2 |^ n) by A3, A6 .= F2 . k by A2, A4, A5, A6, A7 ; ::_thesis: verum end; hence F1 = F2 by A2, A4, A6, FINSEQ_1:13; ::_thesis: verum end; end; :: deftheorem Def4 defines dyad URYSOHN1:def_4_:_ for n being Nat for b2 being FinSequence holds ( b2 = dyad n iff ( dom b2 = Seg ((2 |^ n) + 1) & ( for i being Element of NAT st i in dom b2 holds b2 . i = (i - 1) / (2 |^ n) ) ) ); theorem :: URYSOHN1:4 for n being Element of NAT holds ( dom (dyad n) = Seg ((2 |^ n) + 1) & rng (dyad n) = dyadic n ) proof let n be Element of NAT ; ::_thesis: ( dom (dyad n) = Seg ((2 |^ n) + 1) & rng (dyad n) = dyadic n ) A1: dom (dyad n) = Seg ((2 |^ n) + 1) by Def4; for x being set holds ( x in rng (dyad n) iff x in dyadic n ) proof let x be set ; ::_thesis: ( x in rng (dyad n) iff x in dyadic n ) A2: ( x in rng (dyad n) implies x in dyadic n ) proof assume x in rng (dyad n) ; ::_thesis: x in dyadic n then consider y being set such that A3: y in dom (dyad n) and A4: x = (dyad n) . y by FUNCT_1:def_3; A5: y in Seg ((2 |^ n) + 1) by A3, Def4; reconsider y = y as Element of NAT by A3; A6: 1 <= y by A5, FINSEQ_1:1; y <= (2 |^ n) + 1 by A5, FINSEQ_1:1; then A7: y - 1 <= ((2 |^ n) + 1) - 1 by XREAL_1:13; consider i being Nat such that A8: 1 + i = y by A6, NAT_1:10; ( i in NAT & x = (y - 1) / (2 |^ n) ) by A3, A4, Def4, ORDINAL1:def_12; hence x in dyadic n by A7, A8, Def1; ::_thesis: verum end; ( x in dyadic n implies x in rng (dyad n) ) proof assume A9: x in dyadic n ; ::_thesis: x in rng (dyad n) then reconsider x = x as Real ; consider i being Element of NAT such that A10: i <= 2 |^ n and A11: x = i / (2 |^ n) by A9, Def1; consider y being Element of NAT such that A12: y = i + 1 ; 0 <= i by NAT_1:2; then ( 0 + 1 <= i + 1 & i + 1 <= (2 |^ n) + 1 ) by A10, XREAL_1:6; then A13: y in Seg ((2 |^ n) + 1) by A12, FINSEQ_1:1; then A14: y in dom (dyad n) by Def4; x = (y - 1) / (2 |^ n) by A11, A12; then x = (dyad n) . y by A1, A13, Def4; hence x in rng (dyad n) by A14, FUNCT_1:def_3; ::_thesis: verum end; hence ( x in rng (dyad n) iff x in dyadic n ) by A2; ::_thesis: verum end; hence ( dom (dyad n) = Seg ((2 |^ n) + 1) & rng (dyad n) = dyadic n ) by Def4, TARSKI:1; ::_thesis: verum end; registration cluster DYADIC -> non empty ; coherence not DYADIC is empty proof ex x being set st x in dyadic 0 by XBOOLE_0:def_1; hence not DYADIC is empty by Def2; ::_thesis: verum end; end; registration cluster DOM -> non empty ; coherence not DOM is empty ; end; theorem Th5: :: URYSOHN1:5 for n being Element of NAT holds dyadic n c= dyadic (n + 1) proof let n be Element of NAT ; ::_thesis: dyadic n c= dyadic (n + 1) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dyadic n or x in dyadic (n + 1) ) assume A1: x in dyadic n ; ::_thesis: x in dyadic (n + 1) ex i being Element of NAT st ( i <= 2 |^ (n + 1) & x = i / (2 |^ (n + 1)) ) proof reconsider x = x as Real by A1; consider i being Element of NAT such that A2: ( i <= 2 |^ n & x = i / (2 |^ n) ) by A1, Def1; take i * 2 ; ::_thesis: ( i * 2 <= 2 |^ (n + 1) & x = (i * 2) / (2 |^ (n + 1)) ) 2 |^ (n + 1) = (2 |^ n) * 2 by NEWTON:6; hence ( i * 2 <= 2 |^ (n + 1) & x = (i * 2) / (2 |^ (n + 1)) ) by A2, XCMPLX_1:91, XREAL_1:64; ::_thesis: verum end; hence x in dyadic (n + 1) by Def1; ::_thesis: verum end; theorem Th6: :: URYSOHN1:6 for n being Element of NAT holds ( 0 in dyadic n & 1 in dyadic n ) proof defpred S1[ Element of NAT ] means ( 0 in dyadic $1 & 1 in dyadic $1 ); A1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: ( 0 in dyadic k & 1 in dyadic k ) ; ::_thesis: S1[k + 1] dyadic k c= dyadic (k + 1) by Th5; hence S1[k + 1] by A2; ::_thesis: verum end; A3: S1[ 0 ] by Th2, TARSKI:def_2; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A3, A1); hence for n being Element of NAT holds ( 0 in dyadic n & 1 in dyadic n ) ; ::_thesis: verum end; theorem Th7: :: URYSOHN1:7 for n, i being Element of NAT st 0 < i & i <= 2 |^ n holds ((i * 2) - 1) / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n) proof let n, i be Element of NAT ; ::_thesis: ( 0 < i & i <= 2 |^ n implies ((i * 2) - 1) / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n) ) assume that A1: 0 < i and A2: i <= 2 |^ n ; ::_thesis: ((i * 2) - 1) / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n) A3: 0 * 2 < i * 2 by A1, XREAL_1:68; then consider k being Nat such that A4: i * 2 = k + 1 by NAT_1:6; A5: not ((i * 2) - 1) / (2 |^ (n + 1)) in dyadic n proof assume ((i * 2) - 1) / (2 |^ (n + 1)) in dyadic n ; ::_thesis: contradiction then consider s being Element of NAT such that s <= 2 |^ n and A6: ((i * 2) - 1) / (2 |^ (n + 1)) = s / (2 |^ n) by Def1; A7: 2 |^ n <> 0 by NEWTON:83; 2 |^ (n + 1) <> 0 by NEWTON:83; then ((i * 2) - 1) * (2 |^ n) = s * (2 |^ (n + 1)) by A6, A7, XCMPLX_1:95; then ((i * 2) - 1) * (2 |^ n) = s * ((2 |^ n) * 2) by NEWTON:6; then ((i * 2) - 1) * (2 |^ n) = (s * 2) * (2 |^ n) ; then ((i * 2) - 1) / (2 |^ n) = (s * 2) / (2 |^ n) by A7, XCMPLX_1:94; then (i * 2) + (- 1) = s * 2 by A7, XCMPLX_1:53; then (2 * i) + 0 = (2 * s) + 1 ; hence contradiction by NAT_1:18; ::_thesis: verum end; i * 2 <= (2 |^ n) * 2 by A2, XREAL_1:64; then i * 2 <= 2 |^ (n + 1) by NEWTON:6; then A8: k <= 2 |^ (n + 1) by A4, NAT_1:13; ( k in NAT & 0 <= k ) by A3, A4, NAT_1:13, ORDINAL1:def_12; then ((i * 2) - 1) / (2 |^ (n + 1)) in dyadic (n + 1) by A4, A8, Def1; hence ((i * 2) - 1) / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n) by A5, XBOOLE_0:def_5; ::_thesis: verum end; theorem Th8: :: URYSOHN1:8 for n, i being Element of NAT st 0 <= i & i < 2 |^ n holds ((i * 2) + 1) / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n) proof let n, i be Element of NAT ; ::_thesis: ( 0 <= i & i < 2 |^ n implies ((i * 2) + 1) / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n) ) assume that A1: 0 <= i and A2: i < 2 |^ n ; ::_thesis: ((i * 2) + 1) / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n) A3: 0 + 1 <= i + 1 by A1, XREAL_1:6; consider s being Element of NAT such that A4: s = i + 1 ; A5: (s * 2) - 1 = (i * 2) + (1 + 0) by A4; s <= 2 |^ n by A2, A4, NAT_1:13; hence ((i * 2) + 1) / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n) by A3, A5, Th7; ::_thesis: verum end; theorem Th9: :: URYSOHN1:9 for n being Element of NAT holds 1 / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n) proof let n be Element of NAT ; ::_thesis: 1 / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n) ( (2 * 0) + 1 = 1 & 0 < 2 |^ n ) by NEWTON:83; hence 1 / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n) by Th8; ::_thesis: verum end; definition let n be Nat; let x be Element of dyadic n; func axis x -> Element of NAT means :Def5: :: URYSOHN1:def 5 x = it / (2 |^ n); existence ex b1 being Element of NAT st x = b1 / (2 |^ n) proof consider i being Element of NAT such that i <= 2 |^ n and A1: x = i / (2 |^ n) by Def1; take i ; ::_thesis: x = i / (2 |^ n) thus x = i / (2 |^ n) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Element of NAT st x = b1 / (2 |^ n) & x = b2 / (2 |^ n) holds b1 = b2 proof let i1, i2 be Element of NAT ; ::_thesis: ( x = i1 / (2 |^ n) & x = i2 / (2 |^ n) implies i1 = i2 ) assume A2: ( x = i1 / (2 |^ n) & x = i2 / (2 |^ n) ) ; ::_thesis: i1 = i2 A3: 2 |^ n <> 0 by NEWTON:83; then i1 = (i1 / (2 |^ n)) * (2 |^ n) by XCMPLX_1:87 .= i2 by A2, A3, XCMPLX_1:87 ; hence i1 = i2 ; ::_thesis: verum end; end; :: deftheorem Def5 defines axis URYSOHN1:def_5_:_ for n being Nat for x being Element of dyadic n for b3 being Element of NAT holds ( b3 = axis x iff x = b3 / (2 |^ n) ); theorem Th10: :: URYSOHN1:10 for n being Element of NAT for x being Element of dyadic n holds ( x = (axis x) / (2 |^ n) & axis x <= 2 |^ n ) proof let n be Element of NAT ; ::_thesis: for x being Element of dyadic n holds ( x = (axis x) / (2 |^ n) & axis x <= 2 |^ n ) let x be Element of dyadic n; ::_thesis: ( x = (axis x) / (2 |^ n) & axis x <= 2 |^ n ) ex i being Element of NAT st ( i <= 2 |^ n & x = i / (2 |^ n) ) by Def1; hence ( x = (axis x) / (2 |^ n) & axis x <= 2 |^ n ) by Def5; ::_thesis: verum end; theorem :: URYSOHN1:11 for n being Element of NAT for x being Element of dyadic n holds ( ((axis x) - 1) / (2 |^ n) < x & x < ((axis x) + 1) / (2 |^ n) ) proof let n be Element of NAT ; ::_thesis: for x being Element of dyadic n holds ( ((axis x) - 1) / (2 |^ n) < x & x < ((axis x) + 1) / (2 |^ n) ) let x be Element of dyadic n; ::_thesis: ( ((axis x) - 1) / (2 |^ n) < x & x < ((axis x) + 1) / (2 |^ n) ) A1: ( 0 + (axis x) < 1 + (axis x) & 0 < 2 |^ n ) by NEWTON:83, XREAL_1:8; ( x = (axis x) / (2 |^ n) & (- 1) + (axis x) < 0 + (axis x) ) by Def5, XREAL_1:8; hence ( ((axis x) - 1) / (2 |^ n) < x & x < ((axis x) + 1) / (2 |^ n) ) by A1, XREAL_1:74; ::_thesis: verum end; theorem Th12: :: URYSOHN1:12 for n being Element of NAT for x being Element of dyadic n holds ((axis x) - 1) / (2 |^ n) < ((axis x) + 1) / (2 |^ n) proof let n be Element of NAT ; ::_thesis: for x being Element of dyadic n holds ((axis x) - 1) / (2 |^ n) < ((axis x) + 1) / (2 |^ n) let x be Element of dyadic n; ::_thesis: ((axis x) - 1) / (2 |^ n) < ((axis x) + 1) / (2 |^ n) ( (- 1) + (axis x) < 1 + (axis x) & 0 < 2 |^ n ) by NEWTON:83, XREAL_1:8; hence ((axis x) - 1) / (2 |^ n) < ((axis x) + 1) / (2 |^ n) by XREAL_1:74; ::_thesis: verum end; theorem Th13: :: URYSOHN1:13 for n being Element of NAT for x being Element of dyadic (n + 1) st not x in dyadic n holds ( ((axis x) - 1) / (2 |^ (n + 1)) in dyadic n & ((axis x) + 1) / (2 |^ (n + 1)) in dyadic n ) proof let n be Element of NAT ; ::_thesis: for x being Element of dyadic (n + 1) st not x in dyadic n holds ( ((axis x) - 1) / (2 |^ (n + 1)) in dyadic n & ((axis x) + 1) / (2 |^ (n + 1)) in dyadic n ) let x be Element of dyadic (n + 1); ::_thesis: ( not x in dyadic n implies ( ((axis x) - 1) / (2 |^ (n + 1)) in dyadic n & ((axis x) + 1) / (2 |^ (n + 1)) in dyadic n ) ) assume A1: not x in dyadic n ; ::_thesis: ( ((axis x) - 1) / (2 |^ (n + 1)) in dyadic n & ((axis x) + 1) / (2 |^ (n + 1)) in dyadic n ) thus ((axis x) - 1) / (2 |^ (n + 1)) in dyadic n ::_thesis: ((axis x) + 1) / (2 |^ (n + 1)) in dyadic n proof consider a being Real such that A2: a = ((axis x) - 1) / (2 |^ (n + 1)) ; ex i being Element of NAT st ( i <= 2 |^ n & a = i / (2 |^ n) ) proof consider s being Element of NAT such that A3: s <= 2 |^ (n + 1) and A4: x = s / (2 |^ (n + 1)) by Def1; consider k being Element of NAT such that A5: ( s = 2 * k or s = (2 * k) + 1 ) by SCHEME1:1; now__::_thesis:_(_(_s_=_k_*_2_&_ex_i_being_Element_of_NAT_st_ (_i_<=_2_|^_n_&_a_=_i_/_(2_|^_n)_)_)_or_(_s_=_(k_*_2)_+_1_&_ex_k,_i_being_Element_of_NAT_st_ (_i_<=_2_|^_n_&_a_=_i_/_(2_|^_n)_)_)_) percases ( s = k * 2 or s = (k * 2) + 1 ) by A5; caseA6: s = k * 2 ; ::_thesis: ex i being Element of NAT st ( i <= 2 |^ n & a = i / (2 |^ n) ) then x = (k * 2) / ((2 |^ n) * 2) by A4, NEWTON:6; then A7: x = k / (2 |^ n) by XCMPLX_1:91; k * 2 <= (2 |^ n) * 2 by A3, A6, NEWTON:6; then k <= ((2 |^ n) * 2) / 2 by XREAL_1:77; hence ex i being Element of NAT st ( i <= 2 |^ n & a = i / (2 |^ n) ) by A1, A7, Def1; ::_thesis: verum end; caseA8: s = (k * 2) + 1 ; ::_thesis: ex k, i being Element of NAT st ( i <= 2 |^ n & a = i / (2 |^ n) ) A9: (2 |^ (n + 1)) - 1 <= 2 |^ (n + 1) by XREAL_1:44; k * 2 <= (2 |^ (n + 1)) - 1 by A3, A8, XREAL_1:19; then k * 2 <= 2 |^ (n + 1) by A9, XXREAL_0:2; then k * 2 <= (2 |^ n) * 2 by NEWTON:6; then A10: k <= ((2 |^ n) * 2) / 2 by XREAL_1:77; take k = k; ::_thesis: ex i being Element of NAT st ( i <= 2 |^ n & a = i / (2 |^ n) ) a = (((k * 2) + 1) - 1) / (2 |^ (n + 1)) by A2, A4, A8, Def5 .= (k * 2) / ((2 |^ n) * 2) by NEWTON:6 .= (k / (2 |^ n)) * (2 / 2) by XCMPLX_1:76 .= k / (2 |^ n) ; hence ex i being Element of NAT st ( i <= 2 |^ n & a = i / (2 |^ n) ) by A10; ::_thesis: verum end; end; end; hence ex i being Element of NAT st ( i <= 2 |^ n & a = i / (2 |^ n) ) ; ::_thesis: verum end; hence ((axis x) - 1) / (2 |^ (n + 1)) in dyadic n by A2, Def1; ::_thesis: verum end; thus ((axis x) + 1) / (2 |^ (n + 1)) in dyadic n ::_thesis: verum proof set a = ((axis x) + 1) / (2 |^ (n + 1)); ex i being Element of NAT st ( i <= 2 |^ n & ((axis x) + 1) / (2 |^ (n + 1)) = i / (2 |^ n) ) proof consider s being Element of NAT such that A11: s <= 2 |^ (n + 1) and A12: x = s / (2 |^ (n + 1)) by Def1; consider k being Element of NAT such that A13: ( s = 2 * k or s = (2 * k) + 1 ) by SCHEME1:1; now__::_thesis:_(_(_s_=_k_*_2_&_ex_i_being_Element_of_NAT_st_ (_i_<=_2_|^_n_&_((axis_x)_+_1)_/_(2_|^_(n_+_1))_=_i_/_(2_|^_n)_)_)_or_(_s_=_(k_*_2)_+_1_&_ex_l,_i_being_Element_of_NAT_st_ (_i_<=_2_|^_n_&_((axis_x)_+_1)_/_(2_|^_(n_+_1))_=_i_/_(2_|^_n)_)_)_) percases ( s = k * 2 or s = (k * 2) + 1 ) by A13; caseA14: s = k * 2 ; ::_thesis: ex i being Element of NAT st ( i <= 2 |^ n & ((axis x) + 1) / (2 |^ (n + 1)) = i / (2 |^ n) ) then x = (k * 2) / ((2 |^ n) * 2) by A12, NEWTON:6; then A15: x = k / (2 |^ n) by XCMPLX_1:91; k * 2 <= (2 |^ n) * 2 by A11, A14, NEWTON:6; then k <= ((2 |^ n) * 2) / 2 by XREAL_1:77; hence ex i being Element of NAT st ( i <= 2 |^ n & ((axis x) + 1) / (2 |^ (n + 1)) = i / (2 |^ n) ) by A1, A15, Def1; ::_thesis: verum end; caseA16: s = (k * 2) + 1 ; ::_thesis: ex l, i being Element of NAT st ( i <= 2 |^ n & ((axis x) + 1) / (2 |^ (n + 1)) = i / (2 |^ n) ) consider l being Element of NAT such that A17: l = k + 1 ; s <> 2 |^ (n + 1) proof A18: 2 |^ (n + 1) <> 0 by NEWTON:83; assume s = 2 |^ (n + 1) ; ::_thesis: contradiction then x = 1 by A12, A18, XCMPLX_1:60; hence contradiction by A1, Th6; ::_thesis: verum end; then (((k * 2) + 1) + 1) + (- 1) < 2 |^ (n + 1) by A11, A16, XXREAL_0:1; then l * 2 <= 2 |^ (n + 1) by A17, NAT_1:13; then l * 2 <= (2 |^ n) * 2 by NEWTON:6; then A19: l <= ((2 |^ n) * 2) / 2 by XREAL_1:77; take l = l; ::_thesis: ex i being Element of NAT st ( i <= 2 |^ n & ((axis x) + 1) / (2 |^ (n + 1)) = i / (2 |^ n) ) ((axis x) + 1) / (2 |^ (n + 1)) = (((k * 2) + 1) + 1) / (2 |^ (n + 1)) by A12, A16, Def5 .= ((k + 1) * 2) / ((2 |^ n) * 2) by NEWTON:6 .= ((k + 1) / (2 |^ n)) * (2 / 2) by XCMPLX_1:76 .= l / (2 |^ n) by A17 ; hence ex i being Element of NAT st ( i <= 2 |^ n & ((axis x) + 1) / (2 |^ (n + 1)) = i / (2 |^ n) ) by A19; ::_thesis: verum end; end; end; hence ex i being Element of NAT st ( i <= 2 |^ n & ((axis x) + 1) / (2 |^ (n + 1)) = i / (2 |^ n) ) ; ::_thesis: verum end; hence ((axis x) + 1) / (2 |^ (n + 1)) in dyadic n by Def1; ::_thesis: verum end; end; theorem Th14: :: URYSOHN1:14 for n being Element of NAT for x1, x2 being Element of dyadic n st x1 < x2 holds axis x1 < axis x2 proof let n be Element of NAT ; ::_thesis: for x1, x2 being Element of dyadic n st x1 < x2 holds axis x1 < axis x2 let x1, x2 be Element of dyadic n; ::_thesis: ( x1 < x2 implies axis x1 < axis x2 ) A1: 0 < 2 |^ n by NEWTON:83; ( x1 = (axis x1) / (2 |^ n) & x2 = (axis x2) / (2 |^ n) ) by Th10; hence ( x1 < x2 implies axis x1 < axis x2 ) by A1, XREAL_1:72; ::_thesis: verum end; theorem Th15: :: URYSOHN1:15 for n being Element of NAT for x1, x2 being Element of dyadic n st x1 < x2 holds ( x1 <= ((axis x2) - 1) / (2 |^ n) & ((axis x1) + 1) / (2 |^ n) <= x2 ) proof let n be Element of NAT ; ::_thesis: for x1, x2 being Element of dyadic n st x1 < x2 holds ( x1 <= ((axis x2) - 1) / (2 |^ n) & ((axis x1) + 1) / (2 |^ n) <= x2 ) let x1, x2 be Element of dyadic n; ::_thesis: ( x1 < x2 implies ( x1 <= ((axis x2) - 1) / (2 |^ n) & ((axis x1) + 1) / (2 |^ n) <= x2 ) ) assume A1: x1 < x2 ; ::_thesis: ( x1 <= ((axis x2) - 1) / (2 |^ n) & ((axis x1) + 1) / (2 |^ n) <= x2 ) then axis x1 < axis x2 by Th14; then A2: (axis x1) + 1 <= axis x2 by NAT_1:13; axis x1 < axis x2 by A1, Th14; then (axis x1) + 1 <= axis x2 by NAT_1:13; then A3: axis x1 <= (axis x2) - 1 by XREAL_1:19; 0 < 2 |^ n by NEWTON:83; then A4: ((axis x1) + 1) / (2 |^ n) <= (axis x2) / (2 |^ n) by A2, XREAL_1:72; 0 < 2 |^ n by NEWTON:83; then (axis x1) / (2 |^ n) <= ((axis x2) - 1) / (2 |^ n) by A3, XREAL_1:72; hence ( x1 <= ((axis x2) - 1) / (2 |^ n) & ((axis x1) + 1) / (2 |^ n) <= x2 ) by A4, Th10; ::_thesis: verum end; theorem Th16: :: URYSOHN1:16 for n being Element of NAT for x1, x2 being Element of dyadic (n + 1) st x1 < x2 & not x1 in dyadic n & not x2 in dyadic n holds ((axis x1) + 1) / (2 |^ (n + 1)) <= ((axis x2) - 1) / (2 |^ (n + 1)) proof let n be Element of NAT ; ::_thesis: for x1, x2 being Element of dyadic (n + 1) st x1 < x2 & not x1 in dyadic n & not x2 in dyadic n holds ((axis x1) + 1) / (2 |^ (n + 1)) <= ((axis x2) - 1) / (2 |^ (n + 1)) let x1, x2 be Element of dyadic (n + 1); ::_thesis: ( x1 < x2 & not x1 in dyadic n & not x2 in dyadic n implies ((axis x1) + 1) / (2 |^ (n + 1)) <= ((axis x2) - 1) / (2 |^ (n + 1)) ) assume that A1: x1 < x2 and A2: not x1 in dyadic n and A3: not x2 in dyadic n ; ::_thesis: ((axis x1) + 1) / (2 |^ (n + 1)) <= ((axis x2) - 1) / (2 |^ (n + 1)) consider k2 being Element of NAT such that A4: ( axis x2 = 2 * k2 or axis x2 = (2 * k2) + 1 ) by SCHEME1:1; A5: axis x2 <> k2 * 2 proof assume A6: axis x2 = k2 * 2 ; ::_thesis: contradiction then x2 = (k2 * 2) / (2 |^ (n + 1)) by Th10; then A7: x2 = (k2 * 2) / ((2 |^ n) * 2) by NEWTON:6 .= (k2 / (2 |^ n)) * (2 / 2) by XCMPLX_1:76 .= k2 / (2 |^ n) ; k2 * 2 <= 2 |^ (n + 1) by A6, Th10; then k2 * 2 <= (2 |^ n) * 2 by NEWTON:6; then k2 <= ((2 |^ n) * 2) / 2 by XREAL_1:77; hence contradiction by A3, A7, Def1; ::_thesis: verum end; consider k1 being Element of NAT such that A8: ( axis x1 = 2 * k1 or axis x1 = (2 * k1) + 1 ) by SCHEME1:1; A9: not axis x1 = k1 * 2 proof assume A10: axis x1 = k1 * 2 ; ::_thesis: contradiction then x1 = (k1 * 2) / (2 |^ (n + 1)) by Th10; then A11: x1 = (k1 * 2) / ((2 |^ n) * 2) by NEWTON:6 .= (k1 / (2 |^ n)) * (2 / 2) by XCMPLX_1:76 .= k1 / (2 |^ n) ; k1 * 2 <= 2 |^ (n + 1) by A10, Th10; then k1 * 2 <= (2 |^ n) * 2 by NEWTON:6; then k1 <= ((2 |^ n) * 2) / 2 by XREAL_1:77; hence contradiction by A2, A11, Def1; ::_thesis: verum end; then (k1 * 2) + 1 < (k2 * 2) + 1 by A1, A8, A4, A5, Th14; then ((k1 * 2) + 1) + (- 1) < ((k2 * 2) + 1) + (- 1) by XREAL_1:6; then (k1 * 2) / 2 < (k2 * 2) / 2 by XREAL_1:74; then k1 + 1 <= k2 by NAT_1:13; then ( 0 < 2 |^ (n + 1) & (k1 + 1) * 2 <= k2 * 2 ) by NEWTON:83, XREAL_1:64; hence ((axis x1) + 1) / (2 |^ (n + 1)) <= ((axis x2) - 1) / (2 |^ (n + 1)) by A8, A4, A9, A5, XREAL_1:72; ::_thesis: verum end; begin notation let T be non empty TopSpace; let x be Point of T; synonym Nbhd of x,T for a_neighborhood of x; end; definition let T be non empty TopSpace; let x be Point of T; redefine mode a_neighborhood of x means :: URYSOHN1:def 6 ex A being Subset of T st ( A is open & x in A & A c= it ); compatibility for b1 being Element of bool the carrier of T holds ( b1 is Nbhd of x,T iff ex A being Subset of T st ( A is open & x in A & A c= b1 ) ) proof let S be Subset of T; ::_thesis: ( S is Nbhd of x,T iff ex A being Subset of T st ( A is open & x in A & A c= S ) ) hereby ::_thesis: ( ex A being Subset of T st ( A is open & x in A & A c= S ) implies S is Nbhd of x,T ) assume A1: S is a_neighborhood of x ; ::_thesis: ex N being Element of bool the carrier of T st ( N is open & x in N & N c= S ) take N = Int S; ::_thesis: ( N is open & x in N & N c= S ) thus N is open ; ::_thesis: ( x in N & N c= S ) thus x in N by A1, CONNSP_2:def_1; ::_thesis: N c= S thus N c= S by TOPS_1:16; ::_thesis: verum end; assume ex A being Subset of T st ( A is open & x in A & A c= S ) ; ::_thesis: S is Nbhd of x,T hence x in Int S by TOPS_1:22; :: according to CONNSP_2:def_1 ::_thesis: verum end; end; :: deftheorem defines Nbhd URYSOHN1:def_6_:_ for T being non empty TopSpace for x being Point of T for b3 being Element of bool the carrier of T holds ( b3 is Nbhd of x,T iff ex A being Subset of T st ( A is open & x in A & A c= b3 ) ); theorem Th17: :: URYSOHN1:17 for T being non empty TopSpace for A being Subset of T holds ( A is open iff for x being Point of T st x in A holds ex B being Nbhd of x,T st B c= A ) proof let T be non empty TopSpace; ::_thesis: for A being Subset of T holds ( A is open iff for x being Point of T st x in A holds ex B being Nbhd of x,T st B c= A ) let A be Subset of T; ::_thesis: ( A is open iff for x being Point of T st x in A holds ex B being Nbhd of x,T st B c= A ) thus ( A is open implies for x being Point of T st x in A holds ex B being Nbhd of x,T st B c= A ) ::_thesis: ( ( for x being Point of T st x in A holds ex B being Nbhd of x,T st B c= A ) implies A is open ) proof assume A1: A is open ; ::_thesis: for x being Point of T st x in A holds ex B being Nbhd of x,T st B c= A let x be Point of T; ::_thesis: ( x in A implies ex B being Nbhd of x,T st B c= A ) assume x in A ; ::_thesis: ex B being Nbhd of x,T st B c= A then ex B being Subset of T st ( B is a_neighborhood of x & B c= A ) by A1, CONNSP_2:7; hence ex B being Nbhd of x,T st B c= A ; ::_thesis: verum end; assume A2: for x being Point of T st x in A holds ex B being Nbhd of x,T st B c= A ; ::_thesis: A is open for x being Point of T st x in A holds ex B being Subset of T st ( B is a_neighborhood of x & B c= A ) proof let x be Point of T; ::_thesis: ( x in A implies ex B being Subset of T st ( B is a_neighborhood of x & B c= A ) ) assume x in A ; ::_thesis: ex B being Subset of T st ( B is a_neighborhood of x & B c= A ) then ex B being Nbhd of x,T st B c= A by A2; hence ex B being Subset of T st ( B is a_neighborhood of x & B c= A ) ; ::_thesis: verum end; hence A is open by CONNSP_2:7; ::_thesis: verum end; theorem :: URYSOHN1:18 for T being non empty TopSpace for A being Subset of T st ( for x being Point of T st x in A holds A is Nbhd of x,T ) holds A is open proof let T be non empty TopSpace; ::_thesis: for A being Subset of T st ( for x being Point of T st x in A holds A is Nbhd of x,T ) holds A is open let A be Subset of T; ::_thesis: ( ( for x being Point of T st x in A holds A is Nbhd of x,T ) implies A is open ) assume A1: for x being Point of T st x in A holds A is Nbhd of x,T ; ::_thesis: A is open for x being Point of T st x in A holds ex B being Nbhd of x,T st B c= A proof let x be Point of T; ::_thesis: ( x in A implies ex B being Nbhd of x,T st B c= A ) assume A2: x in A ; ::_thesis: ex B being Nbhd of x,T st B c= A ex B being Nbhd of x,T st B c= A proof A is Nbhd of x,T by A1, A2; then consider B being Nbhd of x,T such that A3: B = A ; take B ; ::_thesis: B c= A thus B c= A by A3; ::_thesis: verum end; hence ex B being Nbhd of x,T st B c= A ; ::_thesis: verum end; hence A is open by Th17; ::_thesis: verum end; definition let T be TopSpace; redefine attr T is T_1 means :Def7: :: URYSOHN1:def 7 for p, q being Point of T st not p = q holds ex W, V being Subset of T st ( W is open & V is open & p in W & not q in W & q in V & not p in V ); compatibility ( T is T_1 iff for p, q being Point of T st not p = q holds ex W, V being Subset of T st ( W is open & V is open & p in W & not q in W & q in V & not p in V ) ) proof thus ( T is T_1 implies for p, q being Point of T st not p = q holds ex W, V being Subset of T st ( W is open & V is open & p in W & not q in W & q in V & not p in V ) ) ::_thesis: ( ( for p, q being Point of T st not p = q holds ex W, V being Subset of T st ( W is open & V is open & p in W & not q in W & q in V & not p in V ) ) implies T is T_1 ) proof assume A1: T is T_1 ; ::_thesis: for p, q being Point of T st not p = q holds ex W, V being Subset of T st ( W is open & V is open & p in W & not q in W & q in V & not p in V ) let p, q be Point of T; ::_thesis: ( not p = q implies ex W, V being Subset of T st ( W is open & V is open & p in W & not q in W & q in V & not p in V ) ) assume A2: not p = q ; ::_thesis: ex W, V being Subset of T st ( W is open & V is open & p in W & not q in W & q in V & not p in V ) consider G1 being Subset of T such that A3: ( G1 is open & p in G1 & q in G1 ` ) by A1, A2, PRE_TOPC:def_9; consider G2 being Subset of T such that A4: ( G2 is open & q in G2 & p in G2 ` ) by A1, A2, PRE_TOPC:def_9; take G1 ; ::_thesis: ex V being Subset of T st ( G1 is open & V is open & p in G1 & not q in G1 & q in V & not p in V ) take G2 ; ::_thesis: ( G1 is open & G2 is open & p in G1 & not q in G1 & q in G2 & not p in G2 ) thus ( G1 is open & G2 is open & p in G1 & not q in G1 & q in G2 & not p in G2 ) by A3, A4, XBOOLE_0:def_5; ::_thesis: verum end; assume A5: for p, q being Point of T st not p = q holds ex W, V being Subset of T st ( W is open & V is open & p in W & not q in W & q in V & not p in V ) ; ::_thesis: T is T_1 let p, q be Point of T; :: according to PRE_TOPC:def_9 ::_thesis: ( p = q or ex b1 being Element of bool the carrier of T st ( b1 is open & p in b1 & q in b1 ` ) ) assume p <> q ; ::_thesis: ex b1 being Element of bool the carrier of T st ( b1 is open & p in b1 & q in b1 ` ) then consider W, V being Subset of T such that A6: W is open and V is open and A7: ( p in W & not q in W ) and q in V and not p in V by A5; take W ; ::_thesis: ( W is open & p in W & q in W ` ) thus ( W is open & p in W & q in W ` ) by A6, A7, XBOOLE_0:def_5; ::_thesis: verum end; end; :: deftheorem Def7 defines T_1 URYSOHN1:def_7_:_ for T being TopSpace holds ( T is T_1 iff for p, q being Point of T st not p = q holds ex W, V being Subset of T st ( W is open & V is open & p in W & not q in W & q in V & not p in V ) ); theorem Th19: :: URYSOHN1:19 for T being non empty TopSpace holds ( T is T_1 iff for p being Point of T holds {p} is closed ) proof let T be non empty TopSpace; ::_thesis: ( T is T_1 iff for p being Point of T holds {p} is closed ) thus ( T is T_1 implies for p being Point of T holds {p} is closed ) ::_thesis: ( ( for p being Point of T holds {p} is closed ) implies T is T_1 ) proof assume A1: T is T_1 ; ::_thesis: for p being Point of T holds {p} is closed for p being Point of T holds {p} is closed proof let p be Point of T; ::_thesis: {p} is closed consider B being Subset of T such that A2: B = {p} ` ; defpred S1[ Subset of T] means ex q being Point of T st ( q in B & ( for V being Subset of T st $1 = V holds ( V is open & q in V & not p in V ) ) ); consider F being Subset-Family of T such that A3: for C being Subset of T holds ( C in F iff S1[C] ) from SUBSET_1:sch_3(); A4: for C being Subset of T holds ( C in F iff ex q being Point of T st ( q in B & C is open & q in C & not p in C ) ) proof let C be Subset of T; ::_thesis: ( C in F iff ex q being Point of T st ( q in B & C is open & q in C & not p in C ) ) A5: ( ex q being Point of T st ( q in B & C is open & q in C & not p in C ) implies C in F ) proof assume A6: ex q being Point of T st ( q in B & C is open & q in C & not p in C ) ; ::_thesis: C in F ex q being Point of T st ( q in B & ( for V being Subset of T st C = V holds ( V is open & q in V & not p in V ) ) ) proof consider q being Point of T such that A7: ( q in B & C is open & q in C & not p in C ) by A6; take q ; ::_thesis: ( q in B & ( for V being Subset of T st C = V holds ( V is open & q in V & not p in V ) ) ) thus ( q in B & ( for V being Subset of T st C = V holds ( V is open & q in V & not p in V ) ) ) by A7; ::_thesis: verum end; hence C in F by A3; ::_thesis: verum end; ( C in F implies ex q being Point of T st ( q in B & C is open & q in C & not p in C ) ) proof assume C in F ; ::_thesis: ex q being Point of T st ( q in B & C is open & q in C & not p in C ) then consider q being Point of T such that A8: ( q in B & ( for V being Subset of T st C = V holds ( V is open & q in V & not p in V ) ) ) by A3; take q ; ::_thesis: ( q in B & C is open & q in C & not p in C ) thus ( q in B & C is open & q in C & not p in C ) by A8; ::_thesis: verum end; hence ( C in F iff ex q being Point of T st ( q in B & C is open & q in C & not p in C ) ) by A5; ::_thesis: verum end; for x being set st x in F holds x in the topology of T proof let x be set ; ::_thesis: ( x in F implies x in the topology of T ) assume A9: x in F ; ::_thesis: x in the topology of T then reconsider x = x as Subset of T ; ex q being Point of T st ( q in B & x is open & q in x & not p in x ) by A4, A9; hence x in the topology of T by PRE_TOPC:def_2; ::_thesis: verum end; then A10: F c= the topology of T by TARSKI:def_3; A11: for q being Point of T st q in B holds ex V being Subset of T st ( V is open & q in V & not p in V ) proof let q be Point of T; ::_thesis: ( q in B implies ex V being Subset of T st ( V is open & q in V & not p in V ) ) assume q in B ; ::_thesis: ex V being Subset of T st ( V is open & q in V & not p in V ) then not q in {p} by A2, XBOOLE_0:def_5; then not q = p by TARSKI:def_1; then ex V, W being Subset of T st ( V is open & W is open & q in V & not p in V & p in W & not q in W ) by A1, Def7; then consider V being Subset of T such that A12: ( V is open & q in V & not p in V ) ; take V ; ::_thesis: ( V is open & q in V & not p in V ) thus ( V is open & q in V & not p in V ) by A12; ::_thesis: verum end; for x being set st x in B holds x in union F proof let x be set ; ::_thesis: ( x in B implies x in union F ) assume A13: x in B ; ::_thesis: x in union F then reconsider x = x as Point of T ; consider C being Subset of T such that A14: ( C is open & x in C & not p in C ) by A11, A13; ex C being set st ( x in C & C in F ) proof take C ; ::_thesis: ( x in C & C in F ) thus ( x in C & C in F ) by A4, A13, A14; ::_thesis: verum end; hence x in union F by TARSKI:def_4; ::_thesis: verum end; then A15: B c= union F by TARSKI:def_3; for x being set st x in union F holds x in B proof let x be set ; ::_thesis: ( x in union F implies x in B ) assume x in union F ; ::_thesis: x in B then consider C being set such that A16: x in C and A17: C in F by TARSKI:def_4; reconsider C = C as Subset of T by A17; ex q being Point of T st ( q in B & C is open & q in C & not p in C ) by A4, A17; then C c= ([#] T) \ {p} by ZFMISC_1:34; hence x in B by A2, A16; ::_thesis: verum end; then union F c= B by TARSKI:def_3; then B = union F by A15, XBOOLE_0:def_10; then B in the topology of T by A10, PRE_TOPC:def_1; then ( {p} ` = ([#] T) \ {p} & B is open ) by PRE_TOPC:def_2; hence {p} is closed by A2, PRE_TOPC:def_3; ::_thesis: verum end; hence for p being Point of T holds {p} is closed ; ::_thesis: verum end; assume A18: for p being Point of T holds {p} is closed ; ::_thesis: T is T_1 for p, q being Point of T st not p = q holds ex W, V being Subset of T st ( W is open & V is open & p in W & not q in W & q in V & not p in V ) proof let p, q be Point of T; ::_thesis: ( not p = q implies ex W, V being Subset of T st ( W is open & V is open & p in W & not q in W & q in V & not p in V ) ) consider V, W being Subset of T such that A19: V = {p} ` and A20: W = {q} ` ; p in {p} by TARSKI:def_1; then A21: not p in V by A19, XBOOLE_0:def_5; assume A22: not p = q ; ::_thesis: ex W, V being Subset of T st ( W is open & V is open & p in W & not q in W & q in V & not p in V ) then not p in {q} by TARSKI:def_1; then A23: p in W by A20, XBOOLE_0:def_5; q in {q} by TARSKI:def_1; then A24: not q in W by A20, XBOOLE_0:def_5; not q in {p} by A22, TARSKI:def_1; then A25: q in V by A19, XBOOLE_0:def_5; ( {p} is closed & {q} is closed ) by A18; hence ex W, V being Subset of T st ( W is open & V is open & p in W & not q in W & q in V & not p in V ) by A19, A20, A23, A24, A25, A21; ::_thesis: verum end; hence T is T_1 by Def7; ::_thesis: verum end; theorem Th20: :: URYSOHN1:20 for T being non empty TopSpace st T is normal holds for A, B being open Subset of T st A <> {} & Cl A c= B holds ex C being Subset of T st ( C <> {} & C is open & Cl A c= C & Cl C c= B ) proof let T be non empty TopSpace; ::_thesis: ( T is normal implies for A, B being open Subset of T st A <> {} & Cl A c= B holds ex C being Subset of T st ( C <> {} & C is open & Cl A c= C & Cl C c= B ) ) assume A1: T is normal ; ::_thesis: for A, B being open Subset of T st A <> {} & Cl A c= B holds ex C being Subset of T st ( C <> {} & C is open & Cl A c= C & Cl C c= B ) let A, B be open Subset of T; ::_thesis: ( A <> {} & Cl A c= B implies ex C being Subset of T st ( C <> {} & C is open & Cl A c= C & Cl C c= B ) ) assume that A2: A <> {} and A3: Cl A c= B ; ::_thesis: ex C being Subset of T st ( C <> {} & C is open & Cl A c= C & Cl C c= B ) now__::_thesis:_(_(_B_<>_[#]_T_&_ex_C,_C_being_Subset_of_T_st_ (_C_<>_{}_&_C_is_open_&_Cl_A_c=_C_&_Cl_C_c=_B_)_)_or_(_B_=_[#]_T_&_ex_C,_C_being_Subset_of_T_st_ (_C_<>_{}_&_C_is_open_&_Cl_A_c=_C_&_Cl_C_c=_B_)_)_) percases ( B <> [#] T or B = [#] T ) ; caseA4: B <> [#] T ; ::_thesis: ex C, C being Subset of T st ( C <> {} & C is open & Cl A c= C & Cl C c= B ) reconsider W = Cl A, V = ([#] T) \ B as Subset of T ; A5: ( W <> {} & V <> {} ) proof A6: ([#] T) \ B <> {} proof assume ([#] T) \ B = {} ; ::_thesis: contradiction then B = ([#] T) \ {} by PRE_TOPC:3; hence contradiction by A4; ::_thesis: verum end; A c= Cl A by PRE_TOPC:18; hence ( W <> {} & V <> {} ) by A2, A6; ::_thesis: verum end; A7: W misses V proof assume W meets V ; ::_thesis: contradiction then consider x being set such that A8: x in W /\ V by XBOOLE_0:4; ( x in Cl A & x in ([#] T) \ B ) by A8, XBOOLE_0:def_4; hence contradiction by A3, XBOOLE_0:def_5; ::_thesis: verum end; B = ([#] T) \ V by PRE_TOPC:3; then V is closed by PRE_TOPC:def_3; then consider C, Q being Subset of T such that A9: C is open and A10: Q is open and A11: W c= C and A12: V c= Q and A13: C misses Q by A1, A5, A7, COMPTS_1:def_3; take C = C; ::_thesis: ex C being Subset of T st ( C <> {} & C is open & Cl A c= C & Cl C c= B ) ( C <> {} & Cl A c= C & Cl C c= B ) proof consider Q0, C0 being Subset of ([#] T) such that A14: ( Q0 = Q & C0 = C ) ; C0 c= Q0 ` by A13, A14, SUBSET_1:23; then Cl C c= Q ` by A10, A14, TOPS_1:5; then Cl C misses Q by SUBSET_1:23; then A15: V misses Cl C by A12, XBOOLE_1:63; (B `) ` = B ; hence ( C <> {} & Cl A c= C & Cl C c= B ) by A5, A11, A15, SUBSET_1:23; ::_thesis: verum end; hence ex C being Subset of T st ( C <> {} & C is open & Cl A c= C & Cl C c= B ) by A9; ::_thesis: verum end; caseA16: B = [#] T ; ::_thesis: ex C, C being Subset of T st ( C <> {} & C is open & Cl A c= C & Cl C c= B ) consider C being Subset of T such that A17: C = [#] T ; take C = C; ::_thesis: ex C being Subset of T st ( C <> {} & C is open & Cl A c= C & Cl C c= B ) Cl C c= B by A16; hence ex C being Subset of T st ( C <> {} & C is open & Cl A c= C & Cl C c= B ) by A17; ::_thesis: verum end; end; end; hence ex C being Subset of T st ( C <> {} & C is open & Cl A c= C & Cl C c= B ) ; ::_thesis: verum end; theorem :: URYSOHN1:21 for T being non empty TopSpace holds ( T is regular iff for A being open Subset of T for p being Point of T st p in A holds ex B being open Subset of T st ( p in B & Cl B c= A ) ) proof let T be non empty TopSpace; ::_thesis: ( T is regular iff for A being open Subset of T for p being Point of T st p in A holds ex B being open Subset of T st ( p in B & Cl B c= A ) ) thus ( T is regular implies for A being open Subset of T for p being Point of T st p in A holds ex B being open Subset of T st ( p in B & Cl B c= A ) ) ::_thesis: ( ( for A being open Subset of T for p being Point of T st p in A holds ex B being open Subset of T st ( p in B & Cl B c= A ) ) implies T is regular ) proof assume A1: T is regular ; ::_thesis: for A being open Subset of T for p being Point of T st p in A holds ex B being open Subset of T st ( p in B & Cl B c= A ) thus for A being open Subset of T for p being Point of T st p in A holds ex B being open Subset of T st ( p in B & Cl B c= A ) ::_thesis: verum proof let A be open Subset of T; ::_thesis: for p being Point of T st p in A holds ex B being open Subset of T st ( p in B & Cl B c= A ) let p be Point of T; ::_thesis: ( p in A implies ex B being open Subset of T st ( p in B & Cl B c= A ) ) assume A2: p in A ; ::_thesis: ex B being open Subset of T st ( p in B & Cl B c= A ) then A3: p in (A `) ` ; thus ex B being open Subset of T st ( p in B & Cl B c= A ) ::_thesis: verum proof reconsider P = A ` as Subset of T ; now__::_thesis:_(_(_P_<>_{}_&_ex_W_being_Subset_of_T_ex_B_being_open_Subset_of_T_st_ (_p_in_B_&_Cl_B_c=_A_)_)_or_(_P_=_{}_&_ex_A,_B_being_open_Subset_of_T_st_ (_p_in_B_&_Cl_B_c=_A_)_)_) percases ( P <> {} or P = {} ) ; case P <> {} ; ::_thesis: ex W being Subset of T ex B being open Subset of T st ( p in B & Cl B c= A ) then consider W, V being Subset of T such that A4: W is open and A5: V is open and A6: p in W and A7: P c= V and A8: W misses V by A1, A3, COMPTS_1:def_2; W /\ V = {} by A8, XBOOLE_0:def_7; then V /\ (Cl W) c= Cl ({} T) by A5, TOPS_1:13; then V /\ (Cl W) c= {} by PRE_TOPC:22; then V /\ (Cl W) = {} ; then V misses Cl W by XBOOLE_0:def_7; then A9: P misses Cl W by A7, XBOOLE_1:63; take W = W; ::_thesis: ex B being open Subset of T st ( p in B & Cl B c= A ) (A `) ` = A ; then Cl W c= A by A9, SUBSET_1:23; hence ex B being open Subset of T st ( p in B & Cl B c= A ) by A4, A6; ::_thesis: verum end; caseA10: P = {} ; ::_thesis: ex A, B being open Subset of T st ( p in B & Cl B c= A ) take A = A; ::_thesis: ex B being open Subset of T st ( p in B & Cl B c= A ) A = [#] T by A10, PRE_TOPC:4; then Cl A c= A ; hence ex B being open Subset of T st ( p in B & Cl B c= A ) by A2; ::_thesis: verum end; end; end; hence ex B being open Subset of T st ( p in B & Cl B c= A ) ; ::_thesis: verum end; end; end; assume A11: for A being open Subset of T for p being Point of T st p in A holds ex B being open Subset of T st ( p in B & Cl B c= A ) ; ::_thesis: T is regular for p being Point of T for P being Subset of T st P <> {} & P is closed & p in P ` holds ex W, V being Subset of T st ( W is open & V is open & p in W & P c= V & W misses V ) proof let p be Point of T; ::_thesis: for P being Subset of T st P <> {} & P is closed & p in P ` holds ex W, V being Subset of T st ( W is open & V is open & p in W & P c= V & W misses V ) let P be Subset of T; ::_thesis: ( P <> {} & P is closed & p in P ` implies ex W, V being Subset of T st ( W is open & V is open & p in W & P c= V & W misses V ) ) assume that P <> {} and A12: ( P is closed & p in P ` ) ; ::_thesis: ex W, V being Subset of T st ( W is open & V is open & p in W & P c= V & W misses V ) thus ex W, V being Subset of T st ( W is open & V is open & p in W & P c= V & W misses V ) ::_thesis: verum proof consider A being Subset of T such that A13: A = P ` ; consider B being open Subset of T such that A14: ( p in B & Cl B c= A ) by A11, A12, A13; consider C being Subset of T such that A15: C = ([#] T) \ (Cl B) ; reconsider B = B, C = C as Subset of T ; Cl B misses C by A15, XBOOLE_1:79; then A16: B misses C by PRE_TOPC:18, XBOOLE_1:63; take B ; ::_thesis: ex V being Subset of T st ( B is open & V is open & p in B & P c= V & B misses V ) take C ; ::_thesis: ( B is open & C is open & p in B & P c= C & B misses C ) ( (Cl B) ` is open & (P `) ` = P ) ; hence ( B is open & C is open & p in B & P c= C & B misses C ) by A13, A14, A15, A16, XBOOLE_1:34; ::_thesis: verum end; end; hence T is regular by COMPTS_1:def_2; ::_thesis: verum end; theorem :: URYSOHN1:22 for T being non empty TopSpace st T is normal & T is T_1 holds for A being open Subset of T st A <> {} holds ex B being Subset of T st ( B <> {} & Cl B c= A ) proof let T be non empty TopSpace; ::_thesis: ( T is normal & T is T_1 implies for A being open Subset of T st A <> {} holds ex B being Subset of T st ( B <> {} & Cl B c= A ) ) assume that A1: T is normal and A2: T is T_1 ; ::_thesis: for A being open Subset of T st A <> {} holds ex B being Subset of T st ( B <> {} & Cl B c= A ) let A be open Subset of T; ::_thesis: ( A <> {} implies ex B being Subset of T st ( B <> {} & Cl B c= A ) ) assume A3: A <> {} ; ::_thesis: ex B being Subset of T st ( B <> {} & Cl B c= A ) now__::_thesis:_(_(_A_<>_[#]_T_&_ex_B,_B_being_Subset_of_T_st_ (_B_<>_{}_&_Cl_B_c=_A_)_)_or_(_A_=_[#]_T_&_ex_B,_B_being_Subset_of_T_st_ (_B_<>_{}_&_Cl_B_c=_A_)_)_) percases ( A <> [#] T or A = [#] T ) ; caseA4: A <> [#] T ; ::_thesis: ex B, B being Subset of T st ( B <> {} & Cl B c= A ) A5: ([#] T) \ A <> {} proof assume ([#] T) \ A = {} ; ::_thesis: contradiction then A = ([#] T) \ {} by PRE_TOPC:3; hence contradiction by A4; ::_thesis: verum end; reconsider V = ([#] T) \ A as Subset of T ; consider x being set such that A6: x in A by A3, XBOOLE_0:def_1; A = ([#] T) \ V by PRE_TOPC:3; then A7: V is closed by PRE_TOPC:def_3; reconsider x = x as Point of T by A6; consider W being set such that A8: W = {x} ; reconsider W = W as Subset of T by A8; A9: W misses V proof assume W meets V ; ::_thesis: contradiction then consider z being set such that A10: z in W /\ V by XBOOLE_0:4; z in W by A10, XBOOLE_0:def_4; then A11: z in A by A6, A8, TARSKI:def_1; z in V by A10, XBOOLE_0:def_4; hence contradiction by A11, XBOOLE_0:def_5; ::_thesis: verum end; W is closed by A2, A8, Th19; then consider B, Q being Subset of T such that B is open and A12: Q is open and A13: W c= B and A14: V c= Q and A15: B misses Q by A1, A8, A7, A5, A9, COMPTS_1:def_3; take B = B; ::_thesis: ex B being Subset of T st ( B <> {} & Cl B c= A ) ( B <> {} & Cl B c= A ) proof B c= Q ` by A15, SUBSET_1:23; then Cl B c= Q ` by A12, TOPS_1:5; then Cl B misses Q by SUBSET_1:23; then A16: V misses Cl B by A14, XBOOLE_1:63; (A `) ` = A ; hence ( B <> {} & Cl B c= A ) by A8, A13, A16, SUBSET_1:23; ::_thesis: verum end; hence ex B being Subset of T st ( B <> {} & Cl B c= A ) ; ::_thesis: verum end; caseA17: A = [#] T ; ::_thesis: ex B, B being Subset of T st ( B <> {} & Cl B c= A ) consider B being Subset of T such that A18: B = [#] T ; take B = B; ::_thesis: ex B being Subset of T st ( B <> {} & Cl B c= A ) Cl B c= A by A17; hence ex B being Subset of T st ( B <> {} & Cl B c= A ) by A18; ::_thesis: verum end; end; end; hence ex B being Subset of T st ( B <> {} & Cl B c= A ) ; ::_thesis: verum end; theorem :: URYSOHN1:23 for T being non empty TopSpace st T is normal holds for A, B being Subset of T st A is open & B is closed & B <> {} & B c= A holds ex C being Subset of T st ( C is open & B c= C & Cl C c= A ) proof let T be non empty TopSpace; ::_thesis: ( T is normal implies for A, B being Subset of T st A is open & B is closed & B <> {} & B c= A holds ex C being Subset of T st ( C is open & B c= C & Cl C c= A ) ) assume A1: T is normal ; ::_thesis: for A, B being Subset of T st A is open & B is closed & B <> {} & B c= A holds ex C being Subset of T st ( C is open & B c= C & Cl C c= A ) let A, B be Subset of T; ::_thesis: ( A is open & B is closed & B <> {} & B c= A implies ex C being Subset of T st ( C is open & B c= C & Cl C c= A ) ) assume that A2: A is open and A3: ( B is closed & B <> {} ) and A4: B c= A ; ::_thesis: ex C being Subset of T st ( C is open & B c= C & Cl C c= A ) percases ( A <> [#] T or A = [#] T ) ; supposeA5: A <> [#] T ; ::_thesis: ex C being Subset of T st ( C is open & B c= C & Cl C c= A ) reconsider V = ([#] T) \ A as Subset of T ; A6: A = ([#] T) \ V by PRE_TOPC:3; then A7: ([#] T) \ A <> {} by A5; A8: B misses V proof assume B /\ V <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction then consider z being set such that A9: z in B /\ V by XBOOLE_0:def_1; ( z in B & z in V ) by A9, XBOOLE_0:def_4; hence contradiction by A4, XBOOLE_0:def_5; ::_thesis: verum end; V is closed by A2, A6, PRE_TOPC:def_3; then consider C, Q being Subset of T such that A10: C is open and A11: Q is open and A12: B c= C and A13: V c= Q and A14: C misses Q by A1, A3, A7, A8, COMPTS_1:def_3; C c= Q ` by A14, SUBSET_1:23; then Cl C c= Q ` by A11, TOPS_1:5; then Q misses Cl C by SUBSET_1:23; then A15: V misses Cl C by A13, XBOOLE_1:63; take C ; ::_thesis: ( C is open & B c= C & Cl C c= A ) thus ( C is open & B c= C ) by A10, A12; ::_thesis: Cl C c= A (A `) ` = A ; hence Cl C c= A by A15, SUBSET_1:23; ::_thesis: verum end; supposeA16: A = [#] T ; ::_thesis: ex C being Subset of T st ( C is open & B c= C & Cl C c= A ) take [#] T ; ::_thesis: ( [#] T is open & B c= [#] T & Cl ([#] T) c= A ) thus ( [#] T is open & B c= [#] T & Cl ([#] T) c= A ) by A16; ::_thesis: verum end; end; end; begin definition let T be non empty TopSpace; let A, B be Subset of T; assume A1: ( T is normal & A <> {} & A is open & B is open & Cl A c= B ) ; mode Between of A,B -> Subset of T means :Def8: :: URYSOHN1:def 8 ( it <> {} & it is open & Cl A c= it & Cl it c= B ); existence ex b1 being Subset of T st ( b1 <> {} & b1 is open & Cl A c= b1 & Cl b1 c= B ) by A1, Th20; end; :: deftheorem Def8 defines Between URYSOHN1:def_8_:_ for T being non empty TopSpace for A, B being Subset of T st T is normal & A <> {} & A is open & B is open & Cl A c= B holds for b4 being Subset of T holds ( b4 is Between of A,B iff ( b4 <> {} & b4 is open & Cl A c= b4 & Cl b4 c= B ) ); theorem :: URYSOHN1:24 for T being non empty TopSpace st T is normal holds for A, B being closed Subset of T st A <> {} holds for n being Element of NAT for 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 ) ) holds ex F being Function of (dyadic (n + 1)),(bool the carrier of T) st ( A c= F . 0 & B = ([#] T) \ (F . 1) & ( for r1, r2, r being Element of dyadic (n + 1) st r1 < r2 holds ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 & ( r in dyadic n implies F . r = G . r ) ) ) ) proof let T be non empty TopSpace; ::_thesis: ( T is normal implies for A, B being closed Subset of T st A <> {} holds for n being Element of NAT for 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 ) ) holds ex F being Function of (dyadic (n + 1)),(bool the carrier of T) st ( A c= F . 0 & B = ([#] T) \ (F . 1) & ( for r1, r2, r being Element of dyadic (n + 1) st r1 < r2 holds ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 & ( r in dyadic n implies F . r = G . r ) ) ) ) ) assume A1: T is normal ; ::_thesis: for A, B being closed Subset of T st A <> {} holds for n being Element of NAT for 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 ) ) holds ex F being Function of (dyadic (n + 1)),(bool the carrier of T) st ( A c= F . 0 & B = ([#] T) \ (F . 1) & ( for r1, r2, r being Element of dyadic (n + 1) st r1 < r2 holds ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 & ( r in dyadic n implies F . r = G . r ) ) ) ) let A, B be closed Subset of T; ::_thesis: ( A <> {} implies for n being Element of NAT for 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 ) ) holds ex F being Function of (dyadic (n + 1)),(bool the carrier of T) st ( A c= F . 0 & B = ([#] T) \ (F . 1) & ( for r1, r2, r being Element of dyadic (n + 1) st r1 < r2 holds ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 & ( r in dyadic n implies F . r = G . r ) ) ) ) ) assume A2: A <> {} ; ::_thesis: for n being Element of NAT for 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 ) ) holds ex F being Function of (dyadic (n + 1)),(bool the carrier of T) st ( A c= F . 0 & B = ([#] T) \ (F . 1) & ( for r1, r2, r being Element of dyadic (n + 1) st r1 < r2 holds ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 & ( r in dyadic n implies F . r = G . r ) ) ) ) let n be Element of NAT ; ::_thesis: for 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 ) ) holds ex F being Function of (dyadic (n + 1)),(bool the carrier of T) st ( A c= F . 0 & B = ([#] T) \ (F . 1) & ( for r1, r2, r being Element of dyadic (n + 1) st r1 < r2 holds ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 & ( r in dyadic n implies F . r = G . r ) ) ) ) let G be Function of (dyadic n),(bool the carrier of T); ::_thesis: ( 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 ) ) implies ex F being Function of (dyadic (n + 1)),(bool the carrier of T) st ( A c= F . 0 & B = ([#] T) \ (F . 1) & ( for r1, r2, r being Element of dyadic (n + 1) st r1 < r2 holds ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 & ( r in dyadic n implies F . r = G . r ) ) ) ) ) assume that A3: A c= G . 0 and A4: B = ([#] T) \ (G . 1) and A5: 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 ) ; ::_thesis: ex F being Function of (dyadic (n + 1)),(bool the carrier of T) st ( A c= F . 0 & B = ([#] T) \ (F . 1) & ( for r1, r2, r being Element of dyadic (n + 1) st r1 < r2 holds ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 & ( r in dyadic n implies F . r = G . r ) ) ) ) A6: for r being Element of dyadic n holds G . r <> {} proof let r be Element of dyadic n; ::_thesis: G . r <> {} percases ( 0 = r or 0 < r ) by Th1; suppose 0 = r ; ::_thesis: G . r <> {} hence G . r <> {} by A2, A3; ::_thesis: verum end; supposeA7: 0 < r ; ::_thesis: G . r <> {} reconsider q1 = 0 as Element of dyadic n by Th6; ( G . q1 c= Cl (G . q1) & Cl (G . q1) c= G . r ) by A5, A7, PRE_TOPC:18; hence G . r <> {} by A2, A3; ::_thesis: verum end; end; end; reconsider S = (dyadic (n + 1)) \ (dyadic n) as non empty set by Th9; A8: ( 0 in dyadic (n + 1) & 1 in dyadic (n + 1) ) by Th6; defpred S1[ Element of S, Subset of T] means for r being Element of dyadic (n + 1) st r in S & $1 = r holds for r1, r2 being Element of dyadic n st r1 = ((axis r) - 1) / (2 |^ (n + 1)) & r2 = ((axis r) + 1) / (2 |^ (n + 1)) holds $2 is Between of G . r1,G . r2; A9: for x being Element of S ex y being Subset of T st S1[x,y] proof let x be Element of S; ::_thesis: ex y being Subset of T st S1[x,y] A10: not x in dyadic n by XBOOLE_0:def_5; reconsider x = x as Element of dyadic (n + 1) by XBOOLE_0:def_5; ( ((axis x) - 1) / (2 |^ (n + 1)) in dyadic n & ((axis x) + 1) / (2 |^ (n + 1)) in dyadic n ) by A10, Th13; then consider q1, q2 being Element of dyadic n such that A11: ( q1 = ((axis x) - 1) / (2 |^ (n + 1)) & q2 = ((axis x) + 1) / (2 |^ (n + 1)) ) ; take the Between of G . q1,G . q2 ; ::_thesis: S1[x, the Between of G . q1,G . q2] thus S1[x, the Between of G . q1,G . q2] by A11; ::_thesis: verum end; consider D being Function of S,(bool the carrier of T) such that A12: for x being Element of S holds S1[x,D . x] from FUNCT_2:sch_3(A9); defpred S2[ Element of dyadic (n + 1), Subset of T] means for r being Element of dyadic (n + 1) st $1 = r holds ( ( r in dyadic n implies $2 = G . r ) & ( not r in dyadic n implies $2 = D . r ) ); A13: for x being Element of dyadic (n + 1) ex y being Subset of T st S2[x,y] proof let x be Element of dyadic (n + 1); ::_thesis: ex y being Subset of T st S2[x,y] percases ( x in dyadic n or not x in dyadic n ) ; suppose x in dyadic n ; ::_thesis: ex y being Subset of T st S2[x,y] then reconsider x = x as Element of dyadic n ; consider y being Subset of T such that A14: y = G . x ; take y ; ::_thesis: S2[x,y] thus S2[x,y] by A14; ::_thesis: verum end; supposeA15: not x in dyadic n ; ::_thesis: ex y being Subset of T st S2[x,y] then reconsider x = x as Element of S by XBOOLE_0:def_5; consider y being Subset of T such that A16: y = D . x ; take y ; ::_thesis: S2[x,y] thus S2[x,y] by A15, A16; ::_thesis: verum end; end; end; consider F being Function of (dyadic (n + 1)),(bool the carrier of T) such that A17: for x being Element of dyadic (n + 1) holds S2[x,F . x] from FUNCT_2:sch_3(A13); take F ; ::_thesis: ( A c= F . 0 & B = ([#] T) \ (F . 1) & ( for r1, r2, r being Element of dyadic (n + 1) st r1 < r2 holds ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 & ( r in dyadic n implies F . r = G . r ) ) ) ) ( 0 in dyadic n & 1 in dyadic n ) by Th6; hence ( A c= F . 0 & B = ([#] T) \ (F . 1) ) by A3, A4, A17, A8; ::_thesis: for r1, r2, r being Element of dyadic (n + 1) st r1 < r2 holds ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 & ( r in dyadic n implies F . r = G . r ) ) let r1, r2, r be Element of dyadic (n + 1); ::_thesis: ( r1 < r2 implies ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 & ( r in dyadic n implies F . r = G . r ) ) ) assume A18: r1 < r2 ; ::_thesis: ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 & ( r in dyadic n implies F . r = G . r ) ) thus ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) ::_thesis: ( r in dyadic n implies F . r = G . r ) proof now__::_thesis:_(_F_._r1_is_open_&_F_._r2_is_open_&_Cl_(F_._r1)_c=_F_._r2_) percases ( ( r1 in dyadic n & r2 in dyadic n ) or ( r1 in dyadic n & not r2 in dyadic n ) or ( not r1 in dyadic n & r2 in dyadic n ) or ( not r1 in dyadic n & not r2 in dyadic n ) ) ; supposeA19: ( r1 in dyadic n & r2 in dyadic n ) ; ::_thesis: ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) then A20: ( F . r1 = G . r1 & F . r2 = G . r2 ) by A17; reconsider r1 = r1, r2 = r2 as Element of dyadic n by A19; r1 < r2 by A18; hence ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) by A5, A20; ::_thesis: verum end; supposeA21: ( r1 in dyadic n & not r2 in dyadic n ) ; ::_thesis: ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) then ( ((axis r2) - 1) / (2 |^ (n + 1)) in dyadic n & ((axis r2) + 1) / (2 |^ (n + 1)) in dyadic n ) by Th13; then consider q1, q2 being Element of dyadic n such that A22: q1 = ((axis r2) - 1) / (2 |^ (n + 1)) and A23: q2 = ((axis r2) + 1) / (2 |^ (n + 1)) ; A24: r1 <= q1 by A18, A22, Th15; r2 in S by A21, XBOOLE_0:def_5; then A25: D . r2 is Between of G . q1,G . q2 by A12, A22, A23; A26: q1 < q2 by A22, A23, Th12; then A27: ( G . q2 is open & Cl (G . q1) c= G . q2 ) by A5; A28: F . r2 = D . r2 by A17, A21; A29: G . q1 <> {} by A6; A30: G . q1 is open by A5, A26; then A31: Cl (G . q1) c= F . r2 by A1, A28, A25, A29, A27, Def8; now__::_thesis:_(_F_._r1_is_open_&_F_._r2_is_open_&_Cl_(F_._r1)_c=_F_._r2_) percases ( r1 = q1 or r1 < q1 ) by A24, XXREAL_0:1; suppose r1 = q1 ; ::_thesis: ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) hence ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) by A1, A17, A28, A25, A29, A30, A27, A31, Def8; ::_thesis: verum end; supposeA32: r1 < q1 ; ::_thesis: ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) A33: G . q1 c= Cl (G . q1) by PRE_TOPC:18; consider q0 being Element of dyadic n such that A34: q0 = r1 by A21; Cl (G . q0) c= G . q1 by A5, A32, A34; then Cl (F . r1) c= G . q1 by A17, A34; then A35: Cl (F . r1) c= Cl (G . q1) by A33, XBOOLE_1:1; A36: G . q0 is open by A5, A32, A34; A37: G . q1 is open by A5, A32, A34; then Cl (G . q1) c= F . r2 by A1, A28, A25, A29, A27, Def8; hence ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) by A1, A17, A28, A25, A29, A27, A34, A36, A37, A35, Def8, XBOOLE_1:1; ::_thesis: verum end; end; end; hence ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) ; ::_thesis: verum end; supposeA38: ( not r1 in dyadic n & r2 in dyadic n ) ; ::_thesis: ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) then ( ((axis r1) - 1) / (2 |^ (n + 1)) in dyadic n & ((axis r1) + 1) / (2 |^ (n + 1)) in dyadic n ) by Th13; then consider q1, q2 being Element of dyadic n such that A39: q1 = ((axis r1) - 1) / (2 |^ (n + 1)) and A40: q2 = ((axis r1) + 1) / (2 |^ (n + 1)) ; A41: q2 <= r2 by A18, A40, Th15; r1 in S by A38, XBOOLE_0:def_5; then A42: D . r1 is Between of G . q1,G . q2 by A12, A39, A40; A43: q1 < q2 by A39, A40, Th12; then A44: ( G . q1 is open & Cl (G . q1) c= G . q2 ) by A5; A45: F . r1 = D . r1 by A17, A38; A46: G . q1 <> {} by A6; A47: G . q2 is open by A5, A43; then A48: Cl (F . r1) c= G . q2 by A1, A45, A42, A46, A44, Def8; now__::_thesis:_(_F_._r1_is_open_&_F_._r2_is_open_&_Cl_(F_._r1)_c=_F_._r2_) percases ( q2 = r2 or q2 < r2 ) by A41, XXREAL_0:1; suppose q2 = r2 ; ::_thesis: ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) hence ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) by A1, A17, A45, A42, A46, A47, A44, A48, Def8; ::_thesis: verum end; supposeA49: q2 < r2 ; ::_thesis: ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) A50: G . q2 c= Cl (G . q2) by PRE_TOPC:18; consider q3 being Element of dyadic n such that A51: q3 = r2 by A38; A52: G . q2 is open by A5, A49, A51; then Cl (F . r1) c= G . q2 by A1, A45, A42, A46, A44, Def8; then A53: Cl (F . r1) c= Cl (G . q2) by A50, XBOOLE_1:1; Cl (G . q2) c= G . q3 by A5, A49, A51; then A54: Cl (G . q2) c= F . r2 by A17, A51; G . q3 is open by A5, A49, A51; hence ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) by A1, A17, A45, A42, A46, A44, A51, A52, A53, A54, Def8, XBOOLE_1:1; ::_thesis: verum end; end; end; hence ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) ; ::_thesis: verum end; supposeA55: ( not r1 in dyadic n & not r2 in dyadic n ) ; ::_thesis: ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) then ( ((axis r1) - 1) / (2 |^ (n + 1)) in dyadic n & ((axis r1) + 1) / (2 |^ (n + 1)) in dyadic n ) by Th13; then consider q11, q21 being Element of dyadic n such that A56: q11 = ((axis r1) - 1) / (2 |^ (n + 1)) and A57: q21 = ((axis r1) + 1) / (2 |^ (n + 1)) ; r1 in S by A55, XBOOLE_0:def_5; then A58: D . r1 is Between of G . q11,G . q21 by A12, A56, A57; A59: q11 < q21 by A56, A57, Th12; then A60: G . q21 is open by A5; ( ((axis r2) - 1) / (2 |^ (n + 1)) in dyadic n & ((axis r2) + 1) / (2 |^ (n + 1)) in dyadic n ) by A55, Th13; then consider q12, q22 being Element of dyadic n such that A61: q12 = ((axis r2) - 1) / (2 |^ (n + 1)) and A62: q22 = ((axis r2) + 1) / (2 |^ (n + 1)) ; r2 in S by A55, XBOOLE_0:def_5; then A63: D . r2 is Between of G . q12,G . q22 by A12, A61, A62; A64: q12 < q22 by A61, A62, Th12; then A65: G . q12 is open by A5; A66: ( G . q22 is open & Cl (G . q12) c= G . q22 ) by A5, A64; A67: G . q12 <> {} by A6; A68: G . q11 <> {} by A6; A69: F . r2 = D . r2 by A17, A55; A70: F . r1 = D . r1 by A17, A55; A71: ( G . q11 is open & Cl (G . q11) c= G . q21 ) by A5, A59; hence ( F . r1 is open & F . r2 is open ) by A1, A70, A58, A68, A60, A69, A63, A67, A65, A66, Def8; ::_thesis: Cl (F . r1) c= F . r2 A72: q21 <= q12 by A18, A55, A57, A61, Th16; now__::_thesis:_Cl_(F_._r1)_c=_F_._r2 percases ( q21 = q12 or q21 < q12 ) by A72, XXREAL_0:1; supposeA73: q21 = q12 ; ::_thesis: Cl (F . r1) c= F . r2 ( Cl (F . r1) c= G . q21 & G . q21 c= Cl (G . q21) ) by A1, A70, A58, A68, A60, A71, Def8, PRE_TOPC:18; then A74: Cl (F . r1) c= Cl (G . q21) by XBOOLE_1:1; Cl (G . q21) c= F . r2 by A1, A60, A69, A63, A67, A66, A73, Def8; hence Cl (F . r1) c= F . r2 by A74, XBOOLE_1:1; ::_thesis: verum end; supposeA75: q21 < q12 ; ::_thesis: Cl (F . r1) c= F . r2 ( Cl (F . r1) c= G . q21 & G . q21 c= Cl (G . q21) ) by A1, A70, A58, A68, A60, A71, Def8, PRE_TOPC:18; then A76: Cl (F . r1) c= Cl (G . q21) by XBOOLE_1:1; Cl (G . q21) c= G . q12 by A5, A75; then A77: Cl (F . r1) c= G . q12 by A76, XBOOLE_1:1; ( G . q12 c= Cl (G . q12) & Cl (G . q12) c= F . r2 ) by A1, A69, A63, A67, A65, A66, Def8, PRE_TOPC:18; then G . q12 c= F . r2 by XBOOLE_1:1; hence Cl (F . r1) c= F . r2 by A77, XBOOLE_1:1; ::_thesis: verum end; end; end; hence Cl (F . r1) c= F . r2 ; ::_thesis: verum end; end; end; hence ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) ; ::_thesis: verum end; thus ( r in dyadic n implies F . r = G . r ) by A17; ::_thesis: verum end;