:: FRECHET semantic presentation
begin
Lm1: for r being Real st r > 0 holds
ex n being Element of NAT st
( 1 / n < r & n > 0 )
proof
let r be Real; ::_thesis: ( r > 0 implies ex n being Element of NAT st
( 1 / n < r & n > 0 ) )
assume A1: r > 0 ; ::_thesis: ex n being Element of NAT st
( 1 / n < r & n > 0 )
consider n being Element of NAT such that
A2: 1 / r < n by SEQ_4:3;
take n ; ::_thesis: ( 1 / n < r & n > 0 )
1 / (1 / r) > 1 / n by A1, A2, XREAL_1:88;
hence 1 / n < r ; ::_thesis: n > 0
thus n > 0 by A1, A2; ::_thesis: verum
end;
theorem :: FRECHET:1
for T being non empty 1-sorted
for S being sequence of T holds rng S is Subset of T ;
theorem Th2: :: FRECHET:2
for T1 being non empty 1-sorted
for T2 being 1-sorted
for S being sequence of T1 st rng S c= the carrier of T2 holds
S is sequence of T2
proof
let T1 be non empty 1-sorted ; ::_thesis: for T2 being 1-sorted
for S being sequence of T1 st rng S c= the carrier of T2 holds
S is sequence of T2
let T2 be 1-sorted ; ::_thesis: for S being sequence of T1 st rng S c= the carrier of T2 holds
S is sequence of T2
let S be sequence of T1; ::_thesis: ( rng S c= the carrier of T2 implies S is sequence of T2 )
A1: dom S = NAT by FUNCT_2:def_1;
assume rng S c= the carrier of T2 ; ::_thesis: S is sequence of T2
hence S is sequence of T2 by A1, FUNCT_2:2; ::_thesis: verum
end;
theorem Th3: :: FRECHET:3
for T being non empty TopSpace
for x being Point of T
for B being Basis of x holds B <> {}
proof
let T be non empty TopSpace; ::_thesis: for x being Point of T
for B being Basis of x holds B <> {}
let x be Point of T; ::_thesis: for B being Basis of x holds B <> {}
let B be Basis of x; ::_thesis: B <> {}
A1: the carrier of T in the topology of T by PRE_TOPC:def_1;
set U1 = [#] T;
reconsider T = T as non empty TopStruct ;
[#] T is open by A1, PRE_TOPC:def_2;
then ex U2 being Subset of T st
( U2 in B & U2 c= [#] T ) by YELLOW_8:13;
hence B <> {} ; ::_thesis: verum
end;
registration
let T be non empty TopSpace;
let x be Point of T;
cluster open x -quasi_basis -> non empty for Element of K19(K19( the carrier of T));
coherence
for b1 being Basis of x holds not b1 is empty by Th3;
end;
Lm2: for T being TopStruct
for A being Subset of T holds
( A is open iff ([#] T) \ A is closed )
proof
let T be TopStruct ; ::_thesis: for A being Subset of T holds
( A is open iff ([#] T) \ A is closed )
let A be Subset of T; ::_thesis: ( A is open iff ([#] T) \ A is closed )
thus ( A is open implies ([#] T) \ A is closed ) ::_thesis: ( ([#] T) \ A is closed implies A is open )
proof
assume A is open ; ::_thesis: ([#] T) \ A is closed
then ([#] T) \ (([#] T) \ A) is open by PRE_TOPC:3;
hence ([#] T) \ A is closed by PRE_TOPC:def_3; ::_thesis: verum
end;
assume ([#] T) \ A is closed ; ::_thesis: A is open
then ([#] T) \ (([#] T) \ A) is open by PRE_TOPC:def_3;
hence A is open by PRE_TOPC:3; ::_thesis: verum
end;
theorem Th4: :: FRECHET:4
for T being TopSpace
for A, B being Subset of T st A is open & B is closed holds
A \ B is open
proof
let T be TopSpace; ::_thesis: for A, B being Subset of T st A is open & B is closed holds
A \ B is open
let A, B be Subset of T; ::_thesis: ( A is open & B is closed implies A \ B is open )
assume that
A1: A is open and
A2: B is closed ; ::_thesis: A \ B is open
([#] T) \ B is open by A2, PRE_TOPC:def_3;
then A /\ (([#] T) \ B) is open by A1, TOPS_1:11;
then A3: (A /\ ([#] T)) \ (A /\ B) is open by XBOOLE_1:50;
A /\ ([#] T) = A by XBOOLE_1:28;
hence A \ B is open by A3, XBOOLE_1:47; ::_thesis: verum
end;
theorem Th5: :: FRECHET:5
for T being TopStruct st {} T is closed & [#] T is closed & ( for A, B being Subset of T st A is closed & B is closed holds
A \/ B is closed ) & ( for F being Subset-Family of T st F is closed holds
meet F is closed ) holds
T is TopSpace
proof
let T be TopStruct ; ::_thesis: ( {} T is closed & [#] T is closed & ( for A, B being Subset of T st A is closed & B is closed holds
A \/ B is closed ) & ( for F being Subset-Family of T st F is closed holds
meet F is closed ) implies T is TopSpace )
assume that
A1: {} T is closed and
A2: [#] T is closed and
A3: for A, B being Subset of T st A is closed & B is closed holds
A \/ B is closed and
A4: for F being Subset-Family of T st F is closed holds
meet F is closed ; ::_thesis: T is TopSpace
A5: for A, B being Subset of T st A in the topology of T & B in the topology of T holds
A /\ B in the topology of T
proof
let A, B be Subset of T; ::_thesis: ( A in the topology of T & B in the topology of T implies A /\ B in the topology of T )
assume that
A6: A in the topology of T and
A7: B in the topology of T ; ::_thesis: A /\ B in the topology of T
reconsider A = A, B = B as Subset of T ;
B is open by A7, PRE_TOPC:def_2;
then A8: ([#] T) \ B is closed by Lm2;
A is open by A6, PRE_TOPC:def_2;
then ([#] T) \ A is closed by Lm2;
then (([#] T) \ A) \/ (([#] T) \ B) is closed by A3, A8;
then ([#] T) \ (A /\ B) is closed by XBOOLE_1:54;
then A /\ B is open by Lm2;
hence A /\ B in the topology of T by PRE_TOPC:def_2; ::_thesis: verum
end;
A9: for G being Subset-Family of T st G c= the topology of T holds
union G in the topology of T
proof
let G be Subset-Family of T; ::_thesis: ( G c= the topology of T implies union G in the topology of T )
reconsider G9 = G as Subset-Family of T ;
assume A10: G c= the topology of T ; ::_thesis: union G in the topology of T
percases ( G = {} or G <> {} ) ;
supposeA11: G = {} ; ::_thesis: union G in the topology of T
([#] T) \ ({} T) = [#] T ;
then {} T is open by A2, Lm2;
hence union G in the topology of T by A11, PRE_TOPC:def_2, ZFMISC_1:2; ::_thesis: verum
end;
supposeA12: G <> {} ; ::_thesis: union G in the topology of T
reconsider CG = COMPLEMENT G as Subset-Family of T ;
A13: for A being Subset of T st A in G holds
([#] T) \ A is closed
proof
let A be Subset of T; ::_thesis: ( A in G implies ([#] T) \ A is closed )
assume A in G ; ::_thesis: ([#] T) \ A is closed
then A is open by A10, PRE_TOPC:def_2;
hence ([#] T) \ A is closed by Lm2; ::_thesis: verum
end;
COMPLEMENT G is closed
proof
let A be Subset of T; :: according to TOPS_2:def_2 ::_thesis: ( not A in COMPLEMENT G or A is closed )
assume A in COMPLEMENT G ; ::_thesis: A is closed
then A ` in G9 by SETFAM_1:def_7;
then ([#] T) \ (A `) is closed by A13;
hence A is closed by PRE_TOPC:3; ::_thesis: verum
end;
then meet CG is closed by A4;
then (union G9) ` is closed by A12, TOPS_2:6;
then ([#] T) \ (union G) is closed ;
then union G is open by Lm2;
hence union G in the topology of T by PRE_TOPC:def_2; ::_thesis: verum
end;
end;
end;
([#] T) \ ({} T) is open by A1, PRE_TOPC:def_3;
then the carrier of T in the topology of T by PRE_TOPC:def_2;
hence T is TopSpace by A9, A5, PRE_TOPC:def_1; ::_thesis: verum
end;
theorem Th6: :: FRECHET:6
for T being TopSpace
for S being non empty TopStruct
for f being Function of T,S st ( for A being Subset of S holds
( A is closed iff f " A is closed ) ) holds
S is TopSpace
proof
let T be TopSpace; ::_thesis: for S being non empty TopStruct
for f being Function of T,S st ( for A being Subset of S holds
( A is closed iff f " A is closed ) ) holds
S is TopSpace
let S be non empty TopStruct ; ::_thesis: for f being Function of T,S st ( for A being Subset of S holds
( A is closed iff f " A is closed ) ) holds
S is TopSpace
let f be Function of T,S; ::_thesis: ( ( for A being Subset of S holds
( A is closed iff f " A is closed ) ) implies S is TopSpace )
assume A1: for A being Subset of S holds
( A is closed iff f " A is closed ) ; ::_thesis: S is TopSpace
A2: for A, B being Subset of S st A is closed & B is closed holds
A \/ B is closed
proof
let A, B be Subset of S; ::_thesis: ( A is closed & B is closed implies A \/ B is closed )
assume ( A is closed & B is closed ) ; ::_thesis: A \/ B is closed
then ( f " A is closed & f " B is closed ) by A1;
then (f " A) \/ (f " B) is closed by TOPS_1:9;
then f " (A \/ B) is closed by RELAT_1:140;
hence A \/ B is closed by A1; ::_thesis: verum
end;
( {} T is closed & f " {} = {} ) ;
then A3: {} S is closed by A1;
A4: for F being Subset-Family of S st F is closed holds
meet F is closed
proof
let F be Subset-Family of S; ::_thesis: ( F is closed implies meet F is closed )
assume A5: F is closed ; ::_thesis: meet F is closed
percases ( F = {} S or F <> {} ) ;
suppose F = {} S ; ::_thesis: meet F is closed
hence meet F is closed by A3, SETFAM_1:def_1; ::_thesis: verum
end;
supposeA6: F <> {} ; ::_thesis: meet F is closed
set F1 = { (f " A) where A is Subset of S : A in F } ;
ex A being set st A in F
proof
set A = the Element of F;
take the Element of F ; ::_thesis: the Element of F in F
thus the Element of F in F by A6; ::_thesis: verum
end;
then consider A being Subset of S such that
A7: A in F ;
reconsider A = A as Subset of S ;
A8: f " A in { (f " A) where A is Subset of S : A in F } by A7;
{ (f " A) where A is Subset of S : A in F } c= bool the carrier of T
proof
let B be set ; :: according to TARSKI:def_3 ::_thesis: ( not B in { (f " A) where A is Subset of S : A in F } or B in bool the carrier of T )
assume B in { (f " A) where A is Subset of S : A in F } ; ::_thesis: B in bool the carrier of T
then ex A being Subset of S st
( B = f " A & A in F ) ;
hence B in bool the carrier of T ; ::_thesis: verum
end;
then reconsider F1 = { (f " A) where A is Subset of S : A in F } as Subset-Family of T ;
A9: meet F1 c= f " (meet F)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet F1 or x in f " (meet F) )
assume A10: x in meet F1 ; ::_thesis: x in f " (meet F)
for A being set st A in F holds
f . x in A
proof
let A be set ; ::_thesis: ( A in F implies f . x in A )
assume A11: A in F ; ::_thesis: f . x in A
then reconsider A = A as Subset of S ;
f " A in F1 by A11;
then x in f " A by A10, SETFAM_1:def_1;
hence f . x in A by FUNCT_1:def_7; ::_thesis: verum
end;
then A12: f . x in meet F by A6, SETFAM_1:def_1;
x in the carrier of T by A10;
then x in dom f by FUNCT_2:def_1;
hence x in f " (meet F) by A12, FUNCT_1:def_7; ::_thesis: verum
end;
F1 is closed
proof
let B be Subset of T; :: according to TOPS_2:def_2 ::_thesis: ( not B in F1 or B is closed )
assume B in F1 ; ::_thesis: B is closed
then consider A being Subset of S such that
A13: f " A = B and
A14: A in F ;
A is closed by A5, A14, TOPS_2:def_2;
hence B is closed by A1, A13; ::_thesis: verum
end;
then A15: meet F1 is closed by TOPS_2:22;
f " (meet F) c= meet F1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f " (meet F) or x in meet F1 )
assume A16: x in f " (meet F) ; ::_thesis: x in meet F1
then A17: f . x in meet F by FUNCT_1:def_7;
A18: x in dom f by A16, FUNCT_1:def_7;
for B being set st B in F1 holds
x in B
proof
let B be set ; ::_thesis: ( B in F1 implies x in B )
assume B in F1 ; ::_thesis: x in B
then consider A being Subset of S such that
A19: B = f " A and
A20: A in F ;
f . x in A by A17, A20, SETFAM_1:def_1;
hence x in B by A18, A19, FUNCT_1:def_7; ::_thesis: verum
end;
hence x in meet F1 by A8, SETFAM_1:def_1; ::_thesis: verum
end;
then meet F1 = f " (meet F) by A9, XBOOLE_0:def_10;
hence meet F is closed by A1, A15; ::_thesis: verum
end;
end;
end;
f " ([#] S) = [#] T by TOPS_2:41;
then [#] S is closed by A1;
hence S is TopSpace by A3, A2, A4, Th5; ::_thesis: verum
end;
theorem Th7: :: FRECHET:7
for x being Point of RealSpace
for r being Real holds Ball (x,r) = ].(x - r),(x + r).[
proof
let x be Point of RealSpace; ::_thesis: for r being Real holds Ball (x,r) = ].(x - r),(x + r).[
let r be Real; ::_thesis: Ball (x,r) = ].(x - r),(x + r).[
reconsider x2 = x as Real by METRIC_1:def_13;
thus Ball (x,r) c= ].(x - r),(x + r).[ :: according to XBOOLE_0:def_10 ::_thesis: ].(x - r),(x + r).[ c= Ball (x,r)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Ball (x,r) or y in ].(x - r),(x + r).[ )
assume A1: y in Ball (x,r) ; ::_thesis: y in ].(x - r),(x + r).[
then reconsider y1 = y as Element of RealSpace ;
reconsider y2 = y1 as Element of REAL by METRIC_1:def_13;
A2: dist (x,y1) = real_dist . (x2,y2) by METRIC_1:def_1, METRIC_1:def_13
.= abs (x2 - y2) by METRIC_1:def_12
.= abs (- (y2 - x2))
.= abs (y2 - x2) by COMPLEX1:52 ;
dist (x,y1) < r by A1, METRIC_1:11;
hence y in ].(x - r),(x + r).[ by A2, RCOMP_1:1; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in ].(x - r),(x + r).[ or y in Ball (x,r) )
assume A3: y in ].(x - r),(x + r).[ ; ::_thesis: y in Ball (x,r)
then reconsider y2 = y as Real ;
reconsider x1 = x, y1 = y2 as Element of RealSpace by METRIC_1:def_13;
abs (y2 - x) = abs (- (y2 - x)) by COMPLEX1:52
.= abs (x - y2)
.= real_dist . (x2,y2) by METRIC_1:def_12 ;
then A4: real_dist . (x2,y2) < r by A3, RCOMP_1:1;
dist (x1,y1) = real_dist . (x2,y2) by METRIC_1:def_1, METRIC_1:def_13;
hence y in Ball (x,r) by A4, METRIC_1:11; ::_thesis: verum
end;
theorem :: FRECHET:8
for A being Subset of R^1 holds
( A is open iff for x being Real st x in A holds
ex r being Real st
( r > 0 & ].(x - r),(x + r).[ c= A ) )
proof
let A be Subset of R^1; ::_thesis: ( A is open iff for x being Real st x in A holds
ex r being Real st
( r > 0 & ].(x - r),(x + r).[ c= A ) )
reconsider A1 = A as Subset of RealSpace by TOPMETR:12;
thus ( A is open implies for x being Real st x in A holds
ex r being Real st
( r > 0 & ].(x - r),(x + r).[ c= A ) ) ::_thesis: ( ( for x being Real st x in A holds
ex r being Real st
( r > 0 & ].(x - r),(x + r).[ c= A ) ) implies A is open )
proof
reconsider A1 = A as Subset of R^1 ;
A1: the topology of R^1 = Family_open_set RealSpace by TOPMETR:12;
assume A is open ; ::_thesis: for x being Real st x in A holds
ex r being Real st
( r > 0 & ].(x - r),(x + r).[ c= A )
then A2: A1 in the topology of R^1 by PRE_TOPC:def_2;
let x be Real; ::_thesis: ( x in A implies ex r being Real st
( r > 0 & ].(x - r),(x + r).[ c= A ) )
reconsider x1 = x as Element of REAL ;
reconsider x1 = x1 as Element of RealSpace by METRIC_1:def_13;
assume x in A ; ::_thesis: ex r being Real st
( r > 0 & ].(x - r),(x + r).[ c= A )
then consider r being Real such that
A3: r > 0 and
A4: Ball (x1,r) c= A1 by A2, A1, PCOMPS_1:def_4;
].(x - r),(x + r).[ c= A1 by A4, Th7;
hence ex r being Real st
( r > 0 & ].(x - r),(x + r).[ c= A ) by A3; ::_thesis: verum
end;
assume A5: for x being Real st x in A holds
ex r being Real st
( r > 0 & ].(x - r),(x + r).[ c= A ) ; ::_thesis: A is open
for x being Element of RealSpace st x in A1 holds
ex r being Real st
( r > 0 & Ball (x,r) c= A1 )
proof
let x be Element of RealSpace; ::_thesis: ( x in A1 implies ex r being Real st
( r > 0 & Ball (x,r) c= A1 ) )
reconsider x1 = x as Real by METRIC_1:def_13;
assume x in A1 ; ::_thesis: ex r being Real st
( r > 0 & Ball (x,r) c= A1 )
then consider r being Real such that
A6: r > 0 and
A7: ].(x1 - r),(x1 + r).[ c= A1 by A5;
Ball (x,r) c= A1 by A7, Th7;
hence ex r being Real st
( r > 0 & Ball (x,r) c= A1 ) by A6; ::_thesis: verum
end;
then A8: A1 in Family_open_set RealSpace by PCOMPS_1:def_4;
the topology of R^1 = Family_open_set RealSpace by TOPMETR:12;
hence A is open by A8, PRE_TOPC:def_2; ::_thesis: verum
end;
theorem Th9: :: FRECHET:9
for S being sequence of R^1 st ( for n being Element of NAT holds S . n in ].(n - (1 / 4)),(n + (1 / 4)).[ ) holds
rng S is closed
proof
let S be sequence of R^1; ::_thesis: ( ( for n being Element of NAT holds S . n in ].(n - (1 / 4)),(n + (1 / 4)).[ ) implies rng S is closed )
reconsider B = rng S as Subset of R^1 ;
assume A1: for n being Element of NAT holds S . n in ].(n - (1 / 4)),(n + (1 / 4)).[ ; ::_thesis: rng S is closed
for x being Point of RealSpace st x in B ` holds
ex r being real number st
( r > 0 & Ball (x,r) c= B ` )
proof
let x be Point of RealSpace; ::_thesis: ( x in B ` implies ex r being real number st
( r > 0 & Ball (x,r) c= B ` ) )
assume A2: x in B ` ; ::_thesis: ex r being real number st
( r > 0 & Ball (x,r) c= B ` )
reconsider x1 = x as Real by METRIC_1:def_13;
percases ( ].(x1 - (1 / 4)),(x1 + (1 / 4)).[ /\ B = {} or ].(x1 - (1 / 4)),(x1 + (1 / 4)).[ /\ B <> {} ) ;
supposeA3: ].(x1 - (1 / 4)),(x1 + (1 / 4)).[ /\ B = {} ; ::_thesis: ex r being real number st
( r > 0 & Ball (x,r) c= B ` )
reconsider C = Ball (x,(1 / 4)) as Subset of R^1 by TOPMETR:12;
(Ball (x,(1 / 4))) /\ ((B `) `) = {} by A3, Th7;
then C misses (B `) ` by XBOOLE_0:def_7;
then Ball (x,(1 / 4)) c= B ` by SUBSET_1:24;
hence ex r being real number st
( r > 0 & Ball (x,r) c= B ` ) ; ::_thesis: verum
end;
supposeA4: ].(x1 - (1 / 4)),(x1 + (1 / 4)).[ /\ B <> {} ; ::_thesis: ex r being real number st
( r > 0 & Ball (x,r) c= B ` )
set y = the Element of ].(x1 - (1 / 4)),(x1 + (1 / 4)).[ /\ B;
A5: the Element of ].(x1 - (1 / 4)),(x1 + (1 / 4)).[ /\ B in ].(x1 - (1 / 4)),(x1 + (1 / 4)).[ by A4, XBOOLE_0:def_4;
A6: the Element of ].(x1 - (1 / 4)),(x1 + (1 / 4)).[ /\ B in B by A4, XBOOLE_0:def_4;
reconsider y = the Element of ].(x1 - (1 / 4)),(x1 + (1 / 4)).[ /\ B as Real by A5;
consider n1 being set such that
A7: n1 in dom S and
A8: y = S . n1 by A6, FUNCT_1:def_3;
reconsider n1 = n1 as Element of NAT by A7;
reconsider r = abs (x1 - y) as Real ;
reconsider C = Ball (x,r) as Subset of R^1 by TOPMETR:12;
abs (y - x1) < 1 / 4 by A5, RCOMP_1:1;
then abs (- (x1 - y)) < 1 / 4 ;
then A9: r <= 1 / 4 by COMPLEX1:52;
Ball (x,r) misses rng S
proof
assume Ball (x,r) meets rng S ; ::_thesis: contradiction
then consider z being set such that
A10: z in Ball (x,r) and
A11: z in rng S by XBOOLE_0:3;
consider n2 being set such that
A12: n2 in dom S and
A13: z = S . n2 by A11, FUNCT_1:def_3;
reconsider n2 = n2 as Element of NAT by A12;
reconsider z = z as Real by A10, METRIC_1:def_13;
percases ( n1 = n2 or n1 > n2 or n1 < n2 ) by XXREAL_0:1;
supposeA14: n1 = n2 ; ::_thesis: contradiction
A15: r = abs (0 + (- (y - x1)))
.= abs (y - x1) by COMPLEX1:52 ;
y in ].(x1 - r),(x1 + r).[ by A8, A10, A13, A14, Th7;
hence contradiction by A15, RCOMP_1:1; ::_thesis: verum
end;
supposeA16: n1 > n2 ; ::_thesis: contradiction
S . n1 in ].(n1 - (1 / 4)),(n1 + (1 / 4)).[ by A1;
then S . n1 in { a where a is Real : ( n1 - (1 / 4) < a & a < n1 + (1 / 4) ) } by RCOMP_1:def_2;
then ex a1 being Real st
( S . n1 = a1 & n1 - (1 / 4) < a1 & a1 < n1 + (1 / 4) ) ;
then A17: n1 < y + (1 / 4) by A8, XREAL_1:19;
S . n2 in ].(n2 - (1 / 4)),(n2 + (1 / 4)).[ by A1;
then S . n2 in { a where a is Real : ( n2 - (1 / 4) < a & a < n2 + (1 / 4) ) } by RCOMP_1:def_2;
then ex a2 being Real st
( S . n2 = a2 & n2 - (1 / 4) < a2 & a2 < n2 + (1 / 4) ) ;
then z - (1 / 4) < n2 by A13, XREAL_1:19;
then A18: n2 + 1 > (z - (1 / 4)) + 1 by XREAL_1:6;
n2 + 1 <= n1 by A16, NAT_1:13;
then n2 + 1 < y + (1 / 4) by A17, XXREAL_0:2;
then z + ((- (1 / 4)) + 1) < y + (1 / 4) by A18, XXREAL_0:2;
then A19: z < (y + (1 / 4)) - ((- (1 / 4)) + 1) by XREAL_1:20;
Ball (x,r) c= Ball (x,(1 / 4)) by A9, PCOMPS_1:1;
then z in Ball (x,(1 / 4)) by A10;
then z in ].(x1 - (1 / 4)),(x1 + (1 / 4)).[ by Th7;
then z in { a where a is Real : ( x1 - (1 / 4) < a & a < x1 + (1 / 4) ) } by RCOMP_1:def_2;
then ex a1 being Real st
( a1 = z & x1 - (1 / 4) < a1 & a1 < x1 + (1 / 4) ) ;
then A20: z + (1 / 4) > x1 by XREAL_1:19;
y in { a where a is Real : ( x1 - (1 / 4) < a & a < x1 + (1 / 4) ) } by A5, RCOMP_1:def_2;
then ex a1 being Real st
( y = a1 & x1 - (1 / 4) < a1 & a1 < x1 + (1 / 4) ) ;
then y - (1 / 4) < (x1 + (1 / 4)) - (1 / 4) by XREAL_1:9;
then z + (1 / 4) > y - (1 / 4) by A20, XXREAL_0:2;
then (z + (1 / 4)) + (- (1 / 4)) > (y - (1 / 4)) + (- (1 / 4)) by XREAL_1:6;
hence contradiction by A19; ::_thesis: verum
end;
supposeA21: n1 < n2 ; ::_thesis: contradiction
S . n2 in ].(n2 - (1 / 4)),(n2 + (1 / 4)).[ by A1;
then S . n2 in { a where a is Real : ( n2 - (1 / 4) < a & a < n2 + (1 / 4) ) } by RCOMP_1:def_2;
then ex a2 being Real st
( S . n2 = a2 & n2 - (1 / 4) < a2 & a2 < n2 + (1 / 4) ) ;
then A22: z + (1 / 4) > (n2 + (- (1 / 4))) + (1 / 4) by A13, XREAL_1:6;
S . n1 in ].(n1 - (1 / 4)),(n1 + (1 / 4)).[ by A1;
then S . n1 in { a where a is Real : ( n1 - (1 / 4) < a & a < n1 + (1 / 4) ) } by RCOMP_1:def_2;
then ex a1 being Real st
( S . n1 = a1 & n1 - (1 / 4) < a1 & a1 < n1 + (1 / 4) ) ;
then (n1 + (1 / 4)) - (1 / 4) > y - (1 / 4) by A8, XREAL_1:9;
then A23: n1 + 1 > (y - (1 / 4)) + 1 by XREAL_1:6;
n1 + 1 <= n2 by A21, NAT_1:13;
then z + (1 / 4) > n1 + 1 by A22, XXREAL_0:2;
then (y + (- (1 / 4))) + 1 < z + (1 / 4) by A23, XXREAL_0:2;
then A24: (y + ((- (1 / 4)) + 1)) - ((- (1 / 4)) + 1) < (z + (1 / 4)) - ((- (1 / 4)) + 1) by XREAL_1:9;
Ball (x,r) c= Ball (x,(1 / 4)) by A9, PCOMPS_1:1;
then z in Ball (x,(1 / 4)) by A10;
then z in ].(x1 - (1 / 4)),(x1 + (1 / 4)).[ by Th7;
then z in { a where a is Real : ( x1 - (1 / 4) < a & a < x1 + (1 / 4) ) } by RCOMP_1:def_2;
then ex a1 being Real st
( a1 = z & x1 - (1 / 4) < a1 & a1 < x1 + (1 / 4) ) ;
then A25: z - (1 / 4) < x1 by XREAL_1:19;
y in { a where a is Real : ( x1 - (1 / 4) < a & a < x1 + (1 / 4) ) } by A5, RCOMP_1:def_2;
then ex a1 being Real st
( y = a1 & x1 - (1 / 4) < a1 & a1 < x1 + (1 / 4) ) ;
then (x1 + (- (1 / 4))) + (1 / 4) < y + (1 / 4) by XREAL_1:6;
then z - (1 / 4) < y + (1 / 4) by A25, XXREAL_0:2;
then (z - (1 / 4)) + (1 / 4) < (y + (1 / 4)) + (1 / 4) by XREAL_1:6;
then z - (1 / 2) < (y + (1 / 2)) - (1 / 2) by XREAL_1:9;
hence contradiction by A24; ::_thesis: verum
end;
end;
end;
then C misses (B `) ` ;
then A26: C c= B ` by SUBSET_1:24;
x1 <> y
proof
assume x1 = y ; ::_thesis: contradiction
then y in B /\ (B `) by A2, A6, XBOOLE_0:def_4;
then B meets B ` by XBOOLE_0:4;
hence contradiction by SUBSET_1:24; ::_thesis: verum
end;
then x1 + (- y) <> y + (- y) ;
then abs (x1 - y) > 0 by COMPLEX1:47;
hence ex r being real number st
( r > 0 & Ball (x,r) c= B ` ) by A26; ::_thesis: verum
end;
end;
end;
then ([#] R^1) \ (rng S) is open by TOPMETR:15;
hence rng S is closed by PRE_TOPC:def_3; ::_thesis: verum
end;
theorem Th10: :: FRECHET:10
for B being Subset of R^1 st B = NAT holds
B is closed
proof
let B be Subset of R^1; ::_thesis: ( B = NAT implies B is closed )
A1: dom (id NAT) = NAT ;
A2: rng (id NAT) = NAT
proof
thus rng (id NAT) c= NAT ; :: according to XBOOLE_0:def_10 ::_thesis: NAT c= rng (id NAT)
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in NAT or y in rng (id NAT) )
assume A3: y in NAT ; ::_thesis: y in rng (id NAT)
thus y in rng (id NAT) by A3; ::_thesis: verum
end;
then reconsider S = id NAT as sequence of R^1 by A1, FUNCT_2:2, TOPMETR:17;
for n being Element of NAT holds S . n in ].(n - (1 / 4)),(n + (1 / 4)).[
proof
let n be Element of NAT ; ::_thesis: S . n in ].(n - (1 / 4)),(n + (1 / 4)).[
reconsider x = S . n as Real by FUNCT_1:17;
A4: (- (1 / 4)) + n < 0 + n by XREAL_1:8;
( x = n & n < n + (1 / 4) ) by FUNCT_1:17, XREAL_1:29;
then x in { r where r is Real : ( n - (1 / 4) < r & r < n + (1 / 4) ) } by A4;
hence S . n in ].(n - (1 / 4)),(n + (1 / 4)).[ by RCOMP_1:def_2; ::_thesis: verum
end;
hence ( B = NAT implies B is closed ) by A2, Th9; ::_thesis: verum
end;
definition
let M be non empty MetrStruct ;
let x be Point of (TopSpaceMetr M);
func Balls x -> Subset-Family of (TopSpaceMetr M) means :Def1: :: FRECHET:def 1
ex y being Point of M st
( y = x & it = { (Ball (y,(1 / n))) where n is Element of NAT : n <> 0 } );
existence
ex b1 being Subset-Family of (TopSpaceMetr M) ex y being Point of M st
( y = x & b1 = { (Ball (y,(1 / n))) where n is Element of NAT : n <> 0 } )
proof
A1: the carrier of M = the carrier of (TopSpaceMetr M) by TOPMETR:12;
then reconsider y = x as Point of M ;
set B = { (Ball (y,(1 / n))) where n is Element of NAT : n <> 0 } ;
{ (Ball (y,(1 / n))) where n is Element of NAT : n <> 0 } c= bool the carrier of (TopSpaceMetr M)
proof
let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in { (Ball (y,(1 / n))) where n is Element of NAT : n <> 0 } or A in bool the carrier of (TopSpaceMetr M) )
assume A in { (Ball (y,(1 / n))) where n is Element of NAT : n <> 0 } ; ::_thesis: A in bool the carrier of (TopSpaceMetr M)
then ex n being Element of NAT st
( A = Ball (y,(1 / n)) & n <> 0 ) ;
hence A in bool the carrier of (TopSpaceMetr M) by A1; ::_thesis: verum
end;
hence ex b1 being Subset-Family of (TopSpaceMetr M) ex y being Point of M st
( y = x & b1 = { (Ball (y,(1 / n))) where n is Element of NAT : n <> 0 } ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset-Family of (TopSpaceMetr M) st ex y being Point of M st
( y = x & b1 = { (Ball (y,(1 / n))) where n is Element of NAT : n <> 0 } ) & ex y being Point of M st
( y = x & b2 = { (Ball (y,(1 / n))) where n is Element of NAT : n <> 0 } ) holds
b1 = b2 ;
end;
:: deftheorem Def1 defines Balls FRECHET:def_1_:_
for M being non empty MetrStruct
for x being Point of (TopSpaceMetr M)
for b3 being Subset-Family of (TopSpaceMetr M) holds
( b3 = Balls x iff ex y being Point of M st
( y = x & b3 = { (Ball (y,(1 / n))) where n is Element of NAT : n <> 0 } ) );
registration
let M be non empty MetrSpace;
let x be Point of (TopSpaceMetr M);
cluster Balls x -> open x -quasi_basis ;
coherence
( Balls x is open & Balls x is x -quasi_basis )
proof
set B = Balls x;
consider x9 being Point of M such that
A1: ( x9 = x & Balls x = { (Ball (x9,(1 / n))) where n is Element of NAT : n <> 0 } ) by Def1;
A2: Balls x c= the topology of (TopSpaceMetr M)
proof
let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in Balls x or A in the topology of (TopSpaceMetr M) )
assume A in Balls x ; ::_thesis: A in the topology of (TopSpaceMetr M)
then consider n being Element of NAT such that
A3: A = Ball (x9,(1 / n)) and
n <> 0 by A1;
Ball (x9,(1 / n)) in Family_open_set M by PCOMPS_1:29;
hence A in the topology of (TopSpaceMetr M) by A3, TOPMETR:12; ::_thesis: verum
end;
A4: for O being set st O in Balls x holds
x in O
proof
let O be set ; ::_thesis: ( O in Balls x implies x in O )
assume O in Balls x ; ::_thesis: x in O
then ex n being Element of NAT st
( O = Ball (x9,(1 / n)) & n <> 0 ) by A1;
hence x in O by A1, GOBOARD6:1; ::_thesis: verum
end;
A5: for O being Subset of (TopSpaceMetr M) st O is open & x in O holds
ex V being Subset of (TopSpaceMetr M) st
( V in Balls x & V c= O )
proof
let O be Subset of (TopSpaceMetr M); ::_thesis: ( O is open & x in O implies ex V being Subset of (TopSpaceMetr M) st
( V in Balls x & V c= O ) )
assume ( O is open & x in O ) ; ::_thesis: ex V being Subset of (TopSpaceMetr M) st
( V in Balls x & V c= O )
then consider r being real number such that
A6: r > 0 and
A7: Ball (x9,r) c= O by A1, TOPMETR:15;
reconsider r = r as Real by XREAL_0:def_1;
consider n being Element of NAT such that
A8: 1 / n < r and
A9: n > 0 by A6, Lm1;
reconsider Ba = Ball (x9,(1 / n)) as Subset of (TopSpaceMetr M) by TOPMETR:12;
reconsider Ba = Ba as Subset of (TopSpaceMetr M) ;
take Ba ; ::_thesis: ( Ba in Balls x & Ba c= O )
thus Ba in Balls x by A1, A9; ::_thesis: Ba c= O
Ball (x9,(1 / n)) c= Ball (x9,r) by A8, PCOMPS_1:1;
hence Ba c= O by A7, XBOOLE_1:1; ::_thesis: verum
end;
A10: Ball (x9,(1 / 1)) in Balls x by A1;
then Intersect (Balls x) = meet (Balls x) by SETFAM_1:def_9;
then x in Intersect (Balls x) by A10, A4, SETFAM_1:def_1;
hence ( Balls x is open & Balls x is x -quasi_basis ) by A2, A5, TOPS_2:64, YELLOW_8:def_1; ::_thesis: verum
end;
end;
registration
let M be non empty MetrSpace;
let x be Point of (TopSpaceMetr M);
cluster Balls x -> countable ;
coherence
Balls x is countable
proof
set B = Balls x;
consider x9 being Point of M such that
A1: ( x9 = x & Balls x = { (Ball (x9,(1 / n))) where n is Element of NAT : n <> 0 } ) by Def1;
deffunc H1( Element of NAT ) -> Element of K19( the carrier of M) = Ball (x9,(1 / M));
defpred S1[ Element of NAT ] means M <> 0 ;
{ H1(n) where n is Element of NAT : S1[n] } is countable from CARD_4:sch_1();
hence Balls x is countable by A1; ::_thesis: verum
end;
end;
theorem Th11: :: FRECHET:11
for M being non empty MetrSpace
for x being Point of (TopSpaceMetr M)
for x9 being Point of M st x = x9 holds
ex f being Function of NAT,(Balls x) st
for n being Element of NAT holds f . n = Ball (x9,(1 / (n + 1)))
proof
let M be non empty MetrSpace; ::_thesis: for x being Point of (TopSpaceMetr M)
for x9 being Point of M st x = x9 holds
ex f being Function of NAT,(Balls x) st
for n being Element of NAT holds f . n = Ball (x9,(1 / (n + 1)))
let x be Point of (TopSpaceMetr M); ::_thesis: for x9 being Point of M st x = x9 holds
ex f being Function of NAT,(Balls x) st
for n being Element of NAT holds f . n = Ball (x9,(1 / (n + 1)))
let x9 be Point of M; ::_thesis: ( x = x9 implies ex f being Function of NAT,(Balls x) st
for n being Element of NAT holds f . n = Ball (x9,(1 / (n + 1))) )
assume A1: x = x9 ; ::_thesis: ex f being Function of NAT,(Balls x) st
for n being Element of NAT holds f . n = Ball (x9,(1 / (n + 1)))
set B = Balls x;
consider x9 being Point of M such that
A2: ( x9 = x & Balls x = { (Ball (x9,(1 / n))) where n is Element of NAT : n <> 0 } ) by Def1;
defpred S1[ set , set ] means ex n9 being Element of NAT st
( $1 = n9 & $2 = Ball (x9,(1 / (n9 + 1))) );
A3: for n being set st n in NAT holds
ex O being set st
( O in Balls x & S1[n,O] )
proof
let n be set ; ::_thesis: ( n in NAT implies ex O being set st
( O in Balls x & S1[n,O] ) )
assume n in NAT ; ::_thesis: ex O being set st
( O in Balls x & S1[n,O] )
then reconsider n = n as Element of NAT ;
take Ball (x9,(1 / (n + 1))) ; ::_thesis: ( Ball (x9,(1 / (n + 1))) in Balls x & S1[n, Ball (x9,(1 / (n + 1)))] )
thus ( Ball (x9,(1 / (n + 1))) in Balls x & S1[n, Ball (x9,(1 / (n + 1)))] ) by A2; ::_thesis: verum
end;
consider f being Function such that
A4: ( dom f = NAT & rng f c= Balls x ) and
A5: for n being set st n in NAT holds
S1[n,f . n] from FUNCT_1:sch_5(A3);
reconsider f = f as Function of NAT,(Balls x) by A4, FUNCT_2:2;
take f ; ::_thesis: for n being Element of NAT holds f . n = Ball (x9,(1 / (n + 1)))
let n be Element of NAT ; ::_thesis: f . n = Ball (x9,(1 / (n + 1)))
S1[n,f . n] by A5;
hence f . n = Ball (x9,(1 / (n + 1))) by A2, A1; ::_thesis: verum
end;
theorem Th12: :: FRECHET:12
for f, g being Function holds rng (f +* g) = (f .: ((dom f) \ (dom g))) \/ (rng g)
proof
let f, g be Function; ::_thesis: rng (f +* g) = (f .: ((dom f) \ (dom g))) \/ (rng g)
thus rng (f +* g) c= (f .: ((dom f) \ (dom g))) \/ (rng g) :: according to XBOOLE_0:def_10 ::_thesis: (f .: ((dom f) \ (dom g))) \/ (rng g) c= rng (f +* g)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (f +* g) or y in (f .: ((dom f) \ (dom g))) \/ (rng g) )
assume y in rng (f +* g) ; ::_thesis: y in (f .: ((dom f) \ (dom g))) \/ (rng g)
then consider x being set such that
A1: x in dom (f +* g) and
A2: (f +* g) . x = y by FUNCT_1:def_3;
percases ( x in dom g or not x in dom g ) ;
supposeA3: x in dom g ; ::_thesis: y in (f .: ((dom f) \ (dom g))) \/ (rng g)
then y = g . x by A2, FUNCT_4:13;
then y in rng g by A3, FUNCT_1:def_3;
hence y in (f .: ((dom f) \ (dom g))) \/ (rng g) by XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA4: not x in dom g ; ::_thesis: y in (f .: ((dom f) \ (dom g))) \/ (rng g)
x in (dom f) \/ (dom g) by A1, FUNCT_4:def_1;
then x in dom f by A4, XBOOLE_0:def_3;
then A5: x in (dom f) \ (dom g) by A4, XBOOLE_0:def_5;
y = f . x by A2, A4, FUNCT_4:11;
then y in f .: ((dom f) \ (dom g)) by A5, FUNCT_1:def_6;
hence y in (f .: ((dom f) \ (dom g))) \/ (rng g) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (f .: ((dom f) \ (dom g))) \/ (rng g) or y in rng (f +* g) )
assume A6: y in (f .: ((dom f) \ (dom g))) \/ (rng g) ; ::_thesis: y in rng (f +* g)
percases ( y in f .: ((dom f) \ (dom g)) or y in rng g ) by A6, XBOOLE_0:def_3;
suppose y in f .: ((dom f) \ (dom g)) ; ::_thesis: y in rng (f +* g)
then consider x being set such that
A7: x in dom f and
A8: x in (dom f) \ (dom g) and
A9: f . x = y by FUNCT_1:def_6;
not x in dom g by A8, XBOOLE_0:def_5;
then A10: (f +* g) . x = f . x by FUNCT_4:11;
x in (dom f) \/ (dom g) by A7, XBOOLE_0:def_3;
then x in dom (f +* g) by FUNCT_4:def_1;
hence y in rng (f +* g) by A9, A10, FUNCT_1:def_3; ::_thesis: verum
end;
supposeA11: y in rng g ; ::_thesis: y in rng (f +* g)
rng g c= rng (f +* g) by FUNCT_4:18;
hence y in rng (f +* g) by A11; ::_thesis: verum
end;
end;
end;
theorem Th13: :: FRECHET:13
for A, B being set st B c= A holds
(id A) .: B = B
proof
let A, B be set ; ::_thesis: ( B c= A implies (id A) .: B = B )
assume A1: B c= A ; ::_thesis: (id A) .: B = B
thus (id A) .: B c= B :: according to XBOOLE_0:def_10 ::_thesis: B c= (id A) .: B
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (id A) .: B or y in B )
assume y in (id A) .: B ; ::_thesis: y in B
then ex x being set st
( x in dom (id A) & x in B & (id A) . x = y ) by FUNCT_1:def_6;
hence y in B by FUNCT_1:17; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in B or y in (id A) .: B )
assume A2: y in B ; ::_thesis: y in (id A) .: B
then ( dom (id A) = A & (id A) . y = y ) by A1, FUNCT_1:17;
hence y in (id A) .: B by A1, A2, FUNCT_1:def_6; ::_thesis: verum
end;
theorem Th14: :: FRECHET:14
for A, B, x being set holds dom ((id A) +* (B --> x)) = A \/ B
proof
let A, B, x be set ; ::_thesis: dom ((id A) +* (B --> x)) = A \/ B
dom ((id A) +* (B --> x)) = (dom (id A)) \/ (dom (B --> x)) by FUNCT_4:def_1;
then dom ((id A) +* (B --> x)) = A \/ (dom (B --> x)) ;
hence dom ((id A) +* (B --> x)) = A \/ B by FUNCOP_1:13; ::_thesis: verum
end;
theorem Th15: :: FRECHET:15
for A, B, x being set st B <> {} holds
rng ((id A) +* (B --> x)) = (A \ B) \/ {x}
proof
let A, B, x be set ; ::_thesis: ( B <> {} implies rng ((id A) +* (B --> x)) = (A \ B) \/ {x} )
set f = (id A) +* (B --> x);
assume B <> {} ; ::_thesis: rng ((id A) +* (B --> x)) = (A \ B) \/ {x}
then A1: rng (B --> x) = {x} by FUNCOP_1:8;
thus rng ((id A) +* (B --> x)) c= (A \ B) \/ {x} :: according to XBOOLE_0:def_10 ::_thesis: (A \ B) \/ {x} c= rng ((id A) +* (B --> x))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ((id A) +* (B --> x)) or y in (A \ B) \/ {x} )
assume y in rng ((id A) +* (B --> x)) ; ::_thesis: y in (A \ B) \/ {x}
then consider x1 being set such that
A2: x1 in dom ((id A) +* (B --> x)) and
A3: y = ((id A) +* (B --> x)) . x1 by FUNCT_1:def_3;
A4: x1 in (dom (id A)) \/ (dom (B --> x)) by A2, FUNCT_4:def_1;
percases ( x1 in dom (B --> x) or not x1 in dom (B --> x) ) ;
suppose x1 in dom (B --> x) ; ::_thesis: y in (A \ B) \/ {x}
then ( ((id A) +* (B --> x)) . x1 = (B --> x) . x1 & (B --> x) . x1 = x ) by A4, FUNCOP_1:7, FUNCT_4:def_1;
then y in {x} by A3, TARSKI:def_1;
hence y in (A \ B) \/ {x} by XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA5: not x1 in dom (B --> x) ; ::_thesis: y in (A \ B) \/ {x}
then A6: ((id A) +* (B --> x)) . x1 = (id A) . x1 by A4, FUNCT_4:def_1;
A7: x1 in dom (id A) by A4, A5, XBOOLE_0:def_3;
not x1 in B by A5, FUNCOP_1:13;
then x1 in A \ B by A7, XBOOLE_0:def_5;
then x1 in (A \ B) \/ {x} by XBOOLE_0:def_3;
hence y in (A \ B) \/ {x} by A3, A6, A7, FUNCT_1:18; ::_thesis: verum
end;
end;
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (A \ B) \/ {x} or y in rng ((id A) +* (B --> x)) )
(id A) .: (A \ B) = A \ B by Th13;
then (id A) .: ((dom (id A)) \ B) = A \ B ;
then A8: (id A) .: ((dom (id A)) \ (dom (B --> x))) = A \ B by FUNCOP_1:13;
assume y in (A \ B) \/ {x} ; ::_thesis: y in rng ((id A) +* (B --> x))
hence y in rng ((id A) +* (B --> x)) by A1, A8, Th12; ::_thesis: verum
end;
theorem Th16: :: FRECHET:16
for A, B, C, x being set st C c= A holds
((id A) +* (B --> x)) " (C \ {x}) = (C \ B) \ {x}
proof
let A, B, C, x be set ; ::_thesis: ( C c= A implies ((id A) +* (B --> x)) " (C \ {x}) = (C \ B) \ {x} )
assume A1: C c= A ; ::_thesis: ((id A) +* (B --> x)) " (C \ {x}) = (C \ B) \ {x}
set f = (id A) +* (B --> x);
thus ((id A) +* (B --> x)) " (C \ {x}) c= (C \ B) \ {x} :: according to XBOOLE_0:def_10 ::_thesis: (C \ B) \ {x} c= ((id A) +* (B --> x)) " (C \ {x})
proof
let x1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x1 in ((id A) +* (B --> x)) " (C \ {x}) or x1 in (C \ B) \ {x} )
assume A2: x1 in ((id A) +* (B --> x)) " (C \ {x}) ; ::_thesis: x1 in (C \ B) \ {x}
then A3: ((id A) +* (B --> x)) . x1 in C \ {x} by FUNCT_1:def_7;
A4: not x1 in B
proof
assume A5: x1 in B ; ::_thesis: contradiction
then A6: x1 in dom (B --> x) by FUNCOP_1:13;
then x1 in (dom (id A)) \/ (dom (B --> x)) by XBOOLE_0:def_3;
then ((id A) +* (B --> x)) . x1 = (B --> x) . x1 by A6, FUNCT_4:def_1;
then A7: ((id A) +* (B --> x)) . x1 = x by A5, FUNCOP_1:7;
not ((id A) +* (B --> x)) . x1 in {x} by A3, XBOOLE_0:def_5;
hence contradiction by A7, TARSKI:def_1; ::_thesis: verum
end;
then A8: not x1 in dom (B --> x) ;
x1 in dom ((id A) +* (B --> x)) by A2, FUNCT_1:def_7;
then x1 in A \/ B by Th14;
then A9: ( x1 in A or x1 in B ) by XBOOLE_0:def_3;
then x1 in dom (id A) by A4;
then x1 in (dom (id A)) \/ (dom (B --> x)) by XBOOLE_0:def_3;
then ((id A) +* (B --> x)) . x1 = (id A) . x1 by A8, FUNCT_4:def_1;
then A10: ((id A) +* (B --> x)) . x1 = x1 by A4, A9, FUNCT_1:17;
then A11: not x1 in {x} by A3, XBOOLE_0:def_5;
x1 in C \ B by A3, A4, A10, XBOOLE_0:def_5;
hence x1 in (C \ B) \ {x} by A11, XBOOLE_0:def_5; ::_thesis: verum
end;
let x1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x1 in (C \ B) \ {x} or x1 in ((id A) +* (B --> x)) " (C \ {x}) )
assume A12: x1 in (C \ B) \ {x} ; ::_thesis: x1 in ((id A) +* (B --> x)) " (C \ {x})
then not x1 in {x} by XBOOLE_0:def_5;
then A13: x1 in C \ {x} by A12, XBOOLE_0:def_5;
A14: x1 in C by A12;
then x1 in A by A1;
then x1 in dom (id A) ;
then A15: x1 in (dom (id A)) \/ (dom (B --> x)) by XBOOLE_0:def_3;
x1 in C \ B by A12, XBOOLE_0:def_5;
then not x1 in dom (B --> x) by XBOOLE_0:def_5;
then ((id A) +* (B --> x)) . x1 = (id A) . x1 by A15, FUNCT_4:def_1;
then A16: ((id A) +* (B --> x)) . x1 = x1 by A1, A14, FUNCT_1:17;
x1 in dom ((id A) +* (B --> x)) by A15, FUNCT_4:def_1;
hence x1 in ((id A) +* (B --> x)) " (C \ {x}) by A13, A16, FUNCT_1:def_7; ::_thesis: verum
end;
theorem Th17: :: FRECHET:17
for A, B, x being set st not x in A holds
((id A) +* (B --> x)) " {x} = B
proof
let A, B, x be set ; ::_thesis: ( not x in A implies ((id A) +* (B --> x)) " {x} = B )
set f = (id A) +* (B --> x);
assume A1: not x in A ; ::_thesis: ((id A) +* (B --> x)) " {x} = B
thus ((id A) +* (B --> x)) " {x} c= B :: according to XBOOLE_0:def_10 ::_thesis: B c= ((id A) +* (B --> x)) " {x}
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in ((id A) +* (B --> x)) " {x} or y in B )
assume A2: y in ((id A) +* (B --> x)) " {x} ; ::_thesis: y in B
then A3: y in dom ((id A) +* (B --> x)) by FUNCT_1:def_7;
A4: ((id A) +* (B --> x)) . y in {x} by A2, FUNCT_1:def_7;
percases ( y in dom (B --> x) or not y in dom (B --> x) ) ;
suppose y in dom (B --> x) ; ::_thesis: y in B
hence y in B ; ::_thesis: verum
end;
supposeA5: not y in dom (B --> x) ; ::_thesis: y in B
then A6: ((id A) +* (B --> x)) . y = (id A) . y by FUNCT_4:11;
A7: ( y in dom (B --> x) or y in dom (id A) ) by A3, FUNCT_4:12;
then (id A) . y = y by A5, FUNCT_1:18;
then y = x by A4, A6, TARSKI:def_1;
hence y in B by A1, A7; ::_thesis: verum
end;
end;
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in B or y in ((id A) +* (B --> x)) " {x} )
assume A8: y in B ; ::_thesis: y in ((id A) +* (B --> x)) " {x}
then A9: y in dom (B --> x) by FUNCOP_1:13;
then ((id A) +* (B --> x)) . y = (B --> x) . y by FUNCT_4:13;
then ((id A) +* (B --> x)) . y = x by A8, FUNCOP_1:7;
then A10: ((id A) +* (B --> x)) . y in {x} by TARSKI:def_1;
y in dom ((id A) +* (B --> x)) by A9, FUNCT_4:12;
hence y in ((id A) +* (B --> x)) " {x} by A10, FUNCT_1:def_7; ::_thesis: verum
end;
theorem Th18: :: FRECHET:18
for A, B, C, x being set st C c= A & not x in A holds
((id A) +* (B --> x)) " (C \/ {x}) = C \/ B
proof
let A, B, C, x be set ; ::_thesis: ( C c= A & not x in A implies ((id A) +* (B --> x)) " (C \/ {x}) = C \/ B )
assume that
A1: C c= A and
A2: not x in A ; ::_thesis: ((id A) +* (B --> x)) " (C \/ {x}) = C \/ B
A3: C \ {x} = C
proof
thus C \ {x} c= C ; :: according to XBOOLE_0:def_10 ::_thesis: C c= C \ {x}
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in C or y in C \ {x} )
assume A4: y in C ; ::_thesis: y in C \ {x}
not y in {x}
proof
assume y in {x} ; ::_thesis: contradiction
then y = x by TARSKI:def_1;
hence contradiction by A1, A2, A4; ::_thesis: verum
end;
hence y in C \ {x} by A4, XBOOLE_0:def_5; ::_thesis: verum
end;
A5: ((C \ B) \ {x}) \/ B = C \/ B
proof
thus ((C \ B) \ {x}) \/ B c= C \/ B :: according to XBOOLE_0:def_10 ::_thesis: C \/ B c= ((C \ B) \ {x}) \/ B
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in ((C \ B) \ {x}) \/ B or y in C \/ B )
assume y in ((C \ B) \ {x}) \/ B ; ::_thesis: y in C \/ B
then ( y in (C \ B) \ {x} or y in B ) by XBOOLE_0:def_3;
hence y in C \/ B by XBOOLE_0:def_3; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in C \/ B or y in ((C \ B) \ {x}) \/ B )
assume y in C \/ B ; ::_thesis: y in ((C \ B) \ {x}) \/ B
then A6: y in (C \ B) \/ B by XBOOLE_1:39;
percases ( y in C \ B or y in B ) by A6, XBOOLE_0:def_3;
supposeA7: y in C \ B ; ::_thesis: y in ((C \ B) \ {x}) \/ B
then A8: y in C ;
not y in {x}
proof
assume y in {x} ; ::_thesis: contradiction
then x in C by A8, TARSKI:def_1;
hence contradiction by A1, A2; ::_thesis: verum
end;
then y in (C \ B) \ {x} by A7, XBOOLE_0:def_5;
hence y in ((C \ B) \ {x}) \/ B by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose y in B ; ::_thesis: y in ((C \ B) \ {x}) \/ B
hence y in ((C \ B) \ {x}) \/ B by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
set f = (id A) +* (B --> x);
((id A) +* (B --> x)) " {x} = B by A2, Th17;
then ((id A) +* (B --> x)) " (C \/ {x}) = (((id A) +* (B --> x)) " C) \/ B by RELAT_1:140;
hence ((id A) +* (B --> x)) " (C \/ {x}) = C \/ B by A1, A3, A5, Th16; ::_thesis: verum
end;
theorem Th19: :: FRECHET:19
for A, B, C, x being set st C c= A & not x in A holds
((id A) +* (B --> x)) " (C \ {x}) = C \ B
proof
let A, B, C, x be set ; ::_thesis: ( C c= A & not x in A implies ((id A) +* (B --> x)) " (C \ {x}) = C \ B )
assume that
A1: C c= A and
A2: not x in A ; ::_thesis: ((id A) +* (B --> x)) " (C \ {x}) = C \ B
not x in C \ B
proof
assume x in C \ B ; ::_thesis: contradiction
then x in C ;
hence contradiction by A1, A2; ::_thesis: verum
end;
then C \ B misses {x} by ZFMISC_1:50;
then (C \ B) \ {x} = C \ B by XBOOLE_1:83;
hence ((id A) +* (B --> x)) " (C \ {x}) = C \ B by A1, Th16; ::_thesis: verum
end;
begin
definition
let T be non empty TopStruct ;
attrT is first-countable means :Def2: :: FRECHET:def 2
for x being Point of T ex B being Basis of x st B is countable ;
end;
:: deftheorem Def2 defines first-countable FRECHET:def_2_:_
for T being non empty TopStruct holds
( T is first-countable iff for x being Point of T ex B being Basis of x st B is countable );
theorem Th20: :: FRECHET:20
for M being non empty MetrSpace holds TopSpaceMetr M is first-countable
proof
let M be non empty MetrSpace; ::_thesis: TopSpaceMetr M is first-countable
let x be Point of (TopSpaceMetr M); :: according to FRECHET:def_2 ::_thesis: ex B being Basis of x st B is countable
take Balls x ; ::_thesis: Balls x is countable
thus Balls x is countable ; ::_thesis: verum
end;
theorem :: FRECHET:21
R^1 is first-countable by Th20;
registration
cluster R^1 -> first-countable ;
coherence
R^1 is first-countable by Th20;
end;
definition
let T be TopStruct ;
let S be sequence of T;
let x be Point of T;
predS is_convergent_to x means :Def3: :: FRECHET:def 3
for U1 being Subset of T st U1 is open & x in U1 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
S . m in U1;
end;
:: deftheorem Def3 defines is_convergent_to FRECHET:def_3_:_
for T being TopStruct
for S being sequence of T
for x being Point of T holds
( S is_convergent_to x iff for U1 being Subset of T st U1 is open & x in U1 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
S . m in U1 );
theorem Th22: :: FRECHET:22
for T being non empty TopStruct
for x being Point of T
for S being sequence of T st S = NAT --> x holds
S is_convergent_to x
proof
let T be non empty TopStruct ; ::_thesis: for x being Point of T
for S being sequence of T st S = NAT --> x holds
S is_convergent_to x
let x be Point of T; ::_thesis: for S being sequence of T st S = NAT --> x holds
S is_convergent_to x
let S be sequence of T; ::_thesis: ( S = NAT --> x implies S is_convergent_to x )
assume A1: S = NAT --> x ; ::_thesis: S is_convergent_to x
thus S is_convergent_to x ::_thesis: verum
proof
let U1 be Subset of T; :: according to FRECHET:def_3 ::_thesis: ( U1 is open & x in U1 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
S . m in U1 )
assume that
U1 is open and
A2: x in U1 ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
S . m in U1
take 0 ; ::_thesis: for m being Element of NAT st 0 <= m holds
S . m in U1
thus for m being Element of NAT st 0 <= m holds
S . m in U1 by A1, A2, FUNCOP_1:7; ::_thesis: verum
end;
end;
definition
let T be TopStruct ;
let S be sequence of T;
attrS is convergent means :Def4: :: FRECHET:def 4
ex x being Point of T st S is_convergent_to x;
end;
:: deftheorem Def4 defines convergent FRECHET:def_4_:_
for T being TopStruct
for S being sequence of T holds
( S is convergent iff ex x being Point of T st S is_convergent_to x );
definition
let T be non empty TopStruct ;
let S be sequence of T;
func Lim S -> Subset of T means :Def5: :: FRECHET:def 5
for x being Point of T holds
( x in it iff S is_convergent_to x );
existence
ex b1 being Subset of T st
for x being Point of T holds
( x in b1 iff S is_convergent_to x )
proof
defpred S1[ Element of T] means S is_convergent_to $1;
{ x where x is Element of T : S1[x] } is Subset of T from DOMAIN_1:sch_7();
then reconsider X = { x where x is Point of T : S1[x] } as Subset of T ;
take X ; ::_thesis: for x being Point of T holds
( x in X iff S is_convergent_to x )
let y be Point of T; ::_thesis: ( y in X iff S is_convergent_to y )
( y in X iff ex x being Point of T st
( x = y & S is_convergent_to x ) ) ;
hence ( y in X iff S is_convergent_to y ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of T st ( for x being Point of T holds
( x in b1 iff S is_convergent_to x ) ) & ( for x being Point of T holds
( x in b2 iff S is_convergent_to x ) ) holds
b1 = b2
proof
let A, B be Subset of T; ::_thesis: ( ( for x being Point of T holds
( x in A iff S is_convergent_to x ) ) & ( for x being Point of T holds
( x in B iff S is_convergent_to x ) ) implies A = B )
assume that
A1: for x being Point of T holds
( x in A iff S is_convergent_to x ) and
A2: for x being Point of T holds
( x in B iff S is_convergent_to x ) ; ::_thesis: A = B
for x being Point of T holds
( x in A iff x in B )
proof
let x be Point of T; ::_thesis: ( x in A iff x in B )
( x in A iff S is_convergent_to x ) by A1;
hence ( x in A iff x in B ) by A2; ::_thesis: verum
end;
hence A = B by SUBSET_1:3; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines Lim FRECHET:def_5_:_
for T being non empty TopStruct
for S being sequence of T
for b3 being Subset of T holds
( b3 = Lim S iff for x being Point of T holds
( x in b3 iff S is_convergent_to x ) );
definition
let T be non empty TopStruct ;
attrT is Frechet means :Def6: :: FRECHET:def 6
for A being Subset of T
for x being Point of T st x in Cl A holds
ex S being sequence of T st
( rng S c= A & x in Lim S );
end;
:: deftheorem Def6 defines Frechet FRECHET:def_6_:_
for T being non empty TopStruct holds
( T is Frechet iff for A being Subset of T
for x being Point of T st x in Cl A holds
ex S being sequence of T st
( rng S c= A & x in Lim S ) );
definition
let T be non empty TopStruct ;
attrT is sequential means :: FRECHET:def 7
for A being Subset of T holds
( A is closed iff for S being sequence of T st S is convergent & rng S c= A holds
Lim S c= A );
end;
:: deftheorem defines sequential FRECHET:def_7_:_
for T being non empty TopStruct holds
( T is sequential iff for A being Subset of T holds
( A is closed iff for S being sequence of T st S is convergent & rng S c= A holds
Lim S c= A ) );
theorem Th23: :: FRECHET:23
for T being non empty TopSpace st T is first-countable holds
T is Frechet
proof
let T be non empty TopSpace; ::_thesis: ( T is first-countable implies T is Frechet )
assume A1: T is first-countable ; ::_thesis: T is Frechet
let A be Subset of T; :: according to FRECHET:def_6 ::_thesis: for x being Point of T st x in Cl A holds
ex S being sequence of T st
( rng S c= A & x in Lim S )
let x be Point of T; ::_thesis: ( x in Cl A implies ex S being sequence of T st
( rng S c= A & x in Lim S ) )
assume A2: x in Cl A ; ::_thesis: ex S being sequence of T st
( rng S c= A & x in Lim S )
consider B being Basis of x such that
A3: B is countable by A1, Def2;
consider f being Function of NAT,B such that
A4: rng f = B by A3, CARD_3:96;
defpred S1[ set , set ] means $2 in A /\ (meet (f .: (succ $1)));
A5: for n being set st n in NAT holds
ex y being set st
( y in the carrier of T & S1[n,y] )
proof
defpred S2[ Element of NAT ] means ex H being Subset of T st
( H = meet (f .: (succ $1)) & H is open );
let n be set ; ::_thesis: ( n in NAT implies ex y being set st
( y in the carrier of T & S1[n,y] ) )
A6: for n being Element of NAT st S2[n] holds
S2[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] )
given G being Subset of T such that A7: G = meet (f .: (succ n)) and
A8: G is open ; ::_thesis: S2[n + 1]
n + 1 in NAT ;
then A9: n + 1 in dom f by FUNCT_2:def_1;
( n in succ n & dom f = NAT ) by FUNCT_2:def_1, ORDINAL1:6;
then A10: f . n in f .: (succ n) by FUNCT_1:def_6;
f . (n + 1) in B ;
then consider H1 being Subset of T such that
A11: H1 = f . (n + 1) ;
A12: H1 is open by A11, YELLOW_8:12;
consider H being Subset of T such that
A13: H = H1 /\ G ;
take H ; ::_thesis: ( H = meet (f .: (succ (n + 1))) & H is open )
meet (f .: (succ (n + 1))) = meet (f .: ({(n + 1)} \/ (n + 1))) by ORDINAL1:def_1
.= meet (f .: ({(n + 1)} \/ (succ n))) by NAT_1:38
.= meet ((Im (f,(n + 1))) \/ (f .: (succ n))) by RELAT_1:120
.= meet ({(f . (n + 1))} \/ (f .: (succ n))) by A9, FUNCT_1:59
.= (meet {(f . (n + 1))}) /\ (meet (f .: (succ n))) by A10, SETFAM_1:9
.= H by A7, A11, A13, SETFAM_1:10 ;
hence ( H = meet (f .: (succ (n + 1))) & H is open ) by A8, A12, A13, TOPS_1:11; ::_thesis: verum
end;
assume n in NAT ; ::_thesis: ex y being set st
( y in the carrier of T & S1[n,y] )
then reconsider n = n as Element of NAT ;
A14: S2[ 0 ]
proof
f . 0 in B ;
then reconsider H = f . 0 as Subset of T ;
take H ; ::_thesis: ( H = meet (f .: (succ 0)) & H is open )
0 in NAT ;
then 0 in dom f by FUNCT_2:def_1;
then meet (Im (f,0)) = meet {(f . 0)} by FUNCT_1:59
.= H by SETFAM_1:10 ;
hence ( H = meet (f .: (succ 0)) & H is open ) by CARD_1:49, YELLOW_8:12; ::_thesis: verum
end;
for n being Element of NAT holds S2[n] from NAT_1:sch_1(A14, A6);
then A15: ex H being Subset of T st
( H = meet (f .: (succ n)) & H is open ) ;
A16: for G being set st G in f .: (succ n) holds
x in G
proof
let G be set ; ::_thesis: ( G in f .: (succ n) implies x in G )
assume G in f .: (succ n) ; ::_thesis: x in G
then consider k being set such that
A17: k in dom f and
k in succ n and
A18: G = f . k by FUNCT_1:def_6;
f . k in B by A17, FUNCT_2:5;
hence x in G by A18, YELLOW_8:12; ::_thesis: verum
end;
( n in succ n & dom f = NAT ) by FUNCT_2:def_1, ORDINAL1:6;
then f . n in f .: (succ n) by FUNCT_1:def_6;
then x in meet (f .: (succ n)) by A16, SETFAM_1:def_1;
then A meets meet (f .: (succ n)) by A2, A15, PRE_TOPC:def_7;
then consider y being set such that
A19: y in A /\ (meet (f .: (succ n))) by XBOOLE_0:4;
take y ; ::_thesis: ( y in the carrier of T & S1[n,y] )
thus ( y in the carrier of T & S1[n,y] ) by A19; ::_thesis: verum
end;
consider S being Function such that
A20: ( dom S = NAT & rng S c= the carrier of T & ( for n being set st n in NAT holds
S1[n,S . n] ) ) from FUNCT_1:sch_5(A5);
A21: rng S c= A
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng S or y in A )
assume y in rng S ; ::_thesis: y in A
then consider a being set such that
A22: ( a in dom S & y = S . a ) by FUNCT_1:def_3;
y in A /\ (meet (f .: (succ a))) by A20, A22;
hence y in A by XBOOLE_0:def_4; ::_thesis: verum
end;
reconsider S = S as sequence of T by A20, FUNCT_2:def_1, RELSET_1:4;
A23: for m, n being Element of NAT st n <= m holds
A /\ (meet (f .: (succ m))) c= A /\ (meet (f .: (succ n)))
proof
let m, n be Element of NAT ; ::_thesis: ( n <= m implies A /\ (meet (f .: (succ m))) c= A /\ (meet (f .: (succ n))) )
assume n <= m ; ::_thesis: A /\ (meet (f .: (succ m))) c= A /\ (meet (f .: (succ n)))
then n + 1 <= m + 1 by XREAL_1:6;
then n + 1 c= m + 1 by NAT_1:39;
then succ n c= m + 1 by NAT_1:38;
then succ n c= succ m by NAT_1:38;
then A24: f .: (succ n) c= f .: (succ m) by RELAT_1:123;
( n in succ n & dom f = NAT ) by FUNCT_2:def_1, ORDINAL1:6;
then f . n in f .: (succ n) by FUNCT_1:def_6;
then meet (f .: (succ m)) c= meet (f .: (succ n)) by A24, SETFAM_1:6;
hence A /\ (meet (f .: (succ m))) c= A /\ (meet (f .: (succ n))) by XBOOLE_1:26; ::_thesis: verum
end;
S is_convergent_to x
proof
let U1 be Subset of T; :: according to FRECHET:def_3 ::_thesis: ( U1 is open & x in U1 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
S . m in U1 )
assume A25: ( U1 is open & x in U1 ) ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
S . m in U1
reconsider U1 = U1 as Subset of T ;
consider U2 being Subset of T such that
A26: U2 in B and
A27: U2 c= U1 by A25, YELLOW_8:13;
consider n being set such that
A28: n in dom f and
A29: U2 = f . n by A4, A26, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A28;
for m being Element of NAT st n <= m holds
S . m in U1
proof
let m be Element of NAT ; ::_thesis: ( n <= m implies S . m in U1 )
( n in succ n & dom f = NAT ) by FUNCT_2:def_1, ORDINAL1:6;
then A30: f . n in f .: (succ n) by FUNCT_1:def_6;
assume n <= m ; ::_thesis: S . m in U1
then A31: A /\ (meet (f .: (succ m))) c= A /\ (meet (f .: (succ n))) by A23;
S . m in A /\ (meet (f .: (succ m))) by A20;
then S . m in meet (f .: (succ n)) by A31, XBOOLE_0:def_4;
then S . m in f . n by A30, SETFAM_1:def_1;
hence S . m in U1 by A27, A29; ::_thesis: verum
end;
hence ex n being Element of NAT st
for m being Element of NAT st n <= m holds
S . m in U1 ; ::_thesis: verum
end;
then x in Lim S by Def5;
hence ex S being sequence of T st
( rng S c= A & x in Lim S ) by A21; ::_thesis: verum
end;
registration
cluster non empty TopSpace-like first-countable -> non empty Frechet for TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is first-countable holds
b1 is Frechet by Th23;
end;
theorem Th24: :: FRECHET:24
for T being non empty TopSpace
for A being Subset of T st A is closed holds
for S being sequence of T st rng S c= A holds
Lim S c= A
proof
let T be non empty TopSpace; ::_thesis: for A being Subset of T st A is closed holds
for S being sequence of T st rng S c= A holds
Lim S c= A
let A be Subset of T; ::_thesis: ( A is closed implies for S being sequence of T st rng S c= A holds
Lim S c= A )
assume A1: A is closed ; ::_thesis: for S being sequence of T st rng S c= A holds
Lim S c= A
let S be sequence of T; ::_thesis: ( rng S c= A implies Lim S c= A )
assume A2: rng S c= A ; ::_thesis: Lim S c= A
thus Lim S c= A ::_thesis: verum
proof
reconsider A = A as Subset of T ;
reconsider L = Lim S as Subset of T ;
L c= A
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in L or y in A )
assume A3: y in L ; ::_thesis: y in A
then reconsider p = y as Point of T ;
A4: S is_convergent_to p by A3, Def5;
for U1 being Subset of T st U1 is open & p in U1 holds
A meets U1
proof
let U1 be Subset of T; ::_thesis: ( U1 is open & p in U1 implies A meets U1 )
assume A5: U1 is open ; ::_thesis: ( not p in U1 or A meets U1 )
reconsider U2 = U1 as Subset of T ;
assume p in U1 ; ::_thesis: A meets U1
then consider n being Element of NAT such that
A6: for m being Element of NAT st n <= m holds
S . m in U2 by A4, A5, Def3;
dom S = NAT by FUNCT_2:def_1;
then A7: S . n in rng S by FUNCT_1:def_3;
S . n in U1 by A6;
then S . n in A /\ U1 by A2, A7, XBOOLE_0:def_4;
hence A meets U1 by XBOOLE_0:def_7; ::_thesis: verum
end;
then p in Cl A by PRE_TOPC:def_7;
hence y in A by A1, PRE_TOPC:22; ::_thesis: verum
end;
hence Lim S c= A ; ::_thesis: verum
end;
end;
theorem Th25: :: FRECHET:25
for T being non empty TopSpace st ( for A being Subset of T st ( for S being sequence of T st S is convergent & rng S c= A holds
Lim S c= A ) holds
A is closed ) holds
T is sequential
proof
let T be non empty TopSpace; ::_thesis: ( ( for A being Subset of T st ( for S being sequence of T st S is convergent & rng S c= A holds
Lim S c= A ) holds
A is closed ) implies T is sequential )
assume A1: for A being Subset of T st ( for S being sequence of T st S is convergent & rng S c= A holds
Lim S c= A ) holds
A is closed ; ::_thesis: T is sequential
let A be Subset of T; :: according to FRECHET:def_7 ::_thesis: ( A is closed iff for S being sequence of T st S is convergent & rng S c= A holds
Lim S c= A )
thus ( A is closed implies for S being sequence of T st S is convergent & rng S c= A holds
Lim S c= A ) by Th24; ::_thesis: ( ( for S being sequence of T st S is convergent & rng S c= A holds
Lim S c= A ) implies A is closed )
assume for S being sequence of T st S is convergent & rng S c= A holds
Lim S c= A ; ::_thesis: A is closed
hence A is closed by A1; ::_thesis: verum
end;
theorem Th26: :: FRECHET:26
for T being non empty TopSpace st T is Frechet holds
T is sequential
proof
let T be non empty TopSpace; ::_thesis: ( T is Frechet implies T is sequential )
assume A1: T is Frechet ; ::_thesis: T is sequential
for A being Subset of T st ( for S being sequence of T st S is convergent & rng S c= A holds
Lim S c= A ) holds
A is closed
proof
let A be Subset of T; ::_thesis: ( ( for S being sequence of T st S is convergent & rng S c= A holds
Lim S c= A ) implies A is closed )
assume A2: for S being sequence of T st S is convergent & rng S c= A holds
Lim S c= A ; ::_thesis: A is closed
A3: Cl A c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Cl A or x in A )
assume A4: x in Cl A ; ::_thesis: x in A
then reconsider p = x as Point of T ;
consider S being sequence of T such that
A5: rng S c= A and
A6: p in Lim S by A1, A4, Def6;
S is_convergent_to p by A6, Def5;
then S is convergent by Def4;
then Lim S c= A by A2, A5;
hence x in A by A6; ::_thesis: verum
end;
A c= Cl A by PRE_TOPC:18;
then A = Cl A by A3, XBOOLE_0:def_10;
hence A is closed by PRE_TOPC:22; ::_thesis: verum
end;
hence T is sequential by Th25; ::_thesis: verum
end;
registration
cluster non empty TopSpace-like Frechet -> non empty sequential for TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is Frechet holds
b1 is sequential by Th26;
end;
begin
definition
func REAL? -> non empty strict TopSpace means :Def8: :: FRECHET:def 8
( the carrier of it = (REAL \ NAT) \/ {REAL} & ex f being Function of R^1,it st
( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of it holds
( A is closed iff f " A is closed ) ) ) );
existence
ex b1 being non empty strict TopSpace st
( the carrier of b1 = (REAL \ NAT) \/ {REAL} & ex f being Function of R^1,b1 st
( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of b1 holds
( A is closed iff f " A is closed ) ) ) )
proof
set f = (id REAL) +* (NAT --> REAL);
reconsider X = (REAL \ NAT) \/ {REAL} as non empty set ;
A1: rng ((id REAL) +* (NAT --> REAL)) c= (REAL \ NAT) \/ {REAL} by Th15;
REAL \/ NAT = REAL by XBOOLE_1:12;
then dom ((id REAL) +* (NAT --> REAL)) = the carrier of R^1 by Th14, TOPMETR:17;
then reconsider f = (id REAL) +* (NAT --> REAL) as Function of the carrier of R^1,X by A1, FUNCT_2:2;
set O = { (X \ A) where A is Subset of X : ex fA being Subset of R^1 st
( fA = f " A & fA is closed ) } ;
{ (X \ A) where A is Subset of X : ex fA being Subset of R^1 st
( fA = f " A & fA is closed ) } c= bool X
proof
let B be set ; :: according to TARSKI:def_3 ::_thesis: ( not B in { (X \ A) where A is Subset of X : ex fA being Subset of R^1 st
( fA = f " A & fA is closed ) } or B in bool X )
assume B in { (X \ A) where A is Subset of X : ex fA being Subset of R^1 st
( fA = f " A & fA is closed ) } ; ::_thesis: B in bool X
then ex A being Subset of X st
( B = X \ A & ex fA being Subset of R^1 st
( fA = f " A & fA is closed ) ) ;
hence B in bool X ; ::_thesis: verum
end;
then reconsider O = { (X \ A) where A is Subset of X : ex fA being Subset of R^1 st
( fA = f " A & fA is closed ) } as Subset-Family of X ;
set T = TopStruct(# X,O #);
reconsider f = f as Function of R^1,TopStruct(# X,O #) ;
A2: for A being Subset of TopStruct(# X,O #) holds
( A is closed iff f " A is closed )
proof
let A be Subset of TopStruct(# X,O #); ::_thesis: ( A is closed iff f " A is closed )
thus ( A is closed implies f " A is closed ) ::_thesis: ( f " A is closed implies A is closed )
proof
assume A is closed ; ::_thesis: f " A is closed
then ([#] TopStruct(# X,O #)) \ A is open by PRE_TOPC:def_3;
then ([#] TopStruct(# X,O #)) \ A in the topology of TopStruct(# X,O #) by PRE_TOPC:def_2;
then consider B being Subset of X such that
A3: X \ B = ([#] TopStruct(# X,O #)) \ A and
A4: ex fA being Subset of R^1 st
( fA = f " B & fA is closed ) ;
B = ([#] TopStruct(# X,O #)) \ (([#] TopStruct(# X,O #)) \ A) by A3, PRE_TOPC:3;
hence f " A is closed by A4, PRE_TOPC:3; ::_thesis: verum
end;
assume f " A is closed ; ::_thesis: A is closed
then X \ A in O ;
then ([#] TopStruct(# X,O #)) \ A is open by PRE_TOPC:def_2;
hence A is closed by PRE_TOPC:def_3; ::_thesis: verum
end;
then reconsider T = TopStruct(# X,O #) as non empty strict TopSpace by Th6;
take T ; ::_thesis: ( the carrier of T = (REAL \ NAT) \/ {REAL} & ex f being Function of R^1,T st
( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of T holds
( A is closed iff f " A is closed ) ) ) )
thus the carrier of T = (REAL \ NAT) \/ {REAL} ; ::_thesis: ex f being Function of R^1,T st
( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of T holds
( A is closed iff f " A is closed ) ) )
reconsider f = f as Function of R^1,T ;
take f ; ::_thesis: ( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of T holds
( A is closed iff f " A is closed ) ) )
thus ( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of T holds
( A is closed iff f " A is closed ) ) ) by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being non empty strict TopSpace st the carrier of b1 = (REAL \ NAT) \/ {REAL} & ex f being Function of R^1,b1 st
( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of b1 holds
( A is closed iff f " A is closed ) ) ) & the carrier of b2 = (REAL \ NAT) \/ {REAL} & ex f being Function of R^1,b2 st
( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of b2 holds
( A is closed iff f " A is closed ) ) ) holds
b1 = b2
proof
let X, Y be non empty strict TopSpace; ::_thesis: ( the carrier of X = (REAL \ NAT) \/ {REAL} & ex f being Function of R^1,X st
( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of X holds
( A is closed iff f " A is closed ) ) ) & the carrier of Y = (REAL \ NAT) \/ {REAL} & ex f being Function of R^1,Y st
( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of Y holds
( A is closed iff f " A is closed ) ) ) implies X = Y )
assume that
A5: the carrier of X = (REAL \ NAT) \/ {REAL} and
A6: ex f being Function of R^1,X st
( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of X holds
( A is closed iff f " A is closed ) ) ) and
A7: the carrier of Y = (REAL \ NAT) \/ {REAL} and
A8: ex f being Function of R^1,Y st
( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of Y holds
( A is closed iff f " A is closed ) ) ) ; ::_thesis: X = Y
consider g being Function of R^1,Y such that
A9: g = (id REAL) +* (NAT --> REAL) and
A10: for A being Subset of Y holds
( A is closed iff g " A is closed ) by A8;
consider f being Function of R^1,X such that
A11: f = (id REAL) +* (NAT --> REAL) and
A12: for A being Subset of X holds
( A is closed iff f " A is closed ) by A6;
A13: the topology of Y c= the topology of X
proof
let V be set ; :: according to TARSKI:def_3 ::_thesis: ( not V in the topology of Y or V in the topology of X )
assume A14: V in the topology of Y ; ::_thesis: V in the topology of X
then reconsider V1 = V as Subset of Y ;
reconsider V2 = V as Subset of X by A5, A7, A14;
reconsider V1 = V1 as Subset of Y ;
reconsider V2 = V2 as Subset of X ;
V1 is open by A14, PRE_TOPC:def_2;
then ([#] Y) \ V1 is closed by Lm2;
then f " (([#] Y) \ V1) is closed by A11, A9, A10;
then ([#] X) \ V2 is closed by A5, A7, A12;
then V2 is open by Lm2;
hence V in the topology of X by PRE_TOPC:def_2; ::_thesis: verum
end;
the topology of X c= the topology of Y
proof
let V be set ; :: according to TARSKI:def_3 ::_thesis: ( not V in the topology of X or V in the topology of Y )
assume A15: V in the topology of X ; ::_thesis: V in the topology of Y
then reconsider V1 = V as Subset of X ;
reconsider V2 = V as Subset of Y by A5, A7, A15;
reconsider V1 = V1 as Subset of X ;
reconsider V2 = V2 as Subset of Y ;
V1 is open by A15, PRE_TOPC:def_2;
then ([#] X) \ V1 is closed by Lm2;
then g " (([#] X) \ V1) is closed by A11, A12, A9;
then ([#] Y) \ V2 is closed by A5, A7, A10;
then V2 is open by Lm2;
hence V in the topology of Y by PRE_TOPC:def_2; ::_thesis: verum
end;
hence X = Y by A5, A7, A13, XBOOLE_0:def_10; ::_thesis: verum
end;
end;
:: deftheorem Def8 defines REAL? FRECHET:def_8_:_
for b1 being non empty strict TopSpace holds
( b1 = REAL? iff ( the carrier of b1 = (REAL \ NAT) \/ {REAL} & ex f being Function of R^1,b1 st
( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of b1 holds
( A is closed iff f " A is closed ) ) ) ) );
Lm3: {REAL} c= the carrier of REAL?
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {REAL} or x in the carrier of REAL? )
assume x in {REAL} ; ::_thesis: x in the carrier of REAL?
then x in (REAL \ NAT) \/ {REAL} by XBOOLE_0:def_3;
hence x in the carrier of REAL? by Def8; ::_thesis: verum
end;
theorem Th27: :: FRECHET:27
REAL is Point of REAL?
proof
REAL in {REAL} by TARSKI:def_1;
hence REAL is Point of REAL? by Lm3; ::_thesis: verum
end;
theorem Th28: :: FRECHET:28
for A being Subset of REAL? holds
( ( A is open & REAL in A ) iff ex O being Subset of R^1 st
( O is open & NAT c= O & A = (O \ NAT) \/ {REAL} ) )
proof
let A be Subset of REAL?; ::_thesis: ( ( A is open & REAL in A ) iff ex O being Subset of R^1 st
( O is open & NAT c= O & A = (O \ NAT) \/ {REAL} ) )
consider f being Function of R^1,REAL? such that
A1: f = (id REAL) +* (NAT --> REAL) and
A2: for A being Subset of REAL? holds
( A is closed iff f " A is closed ) by Def8;
thus ( A is open & REAL in A implies ex O being Subset of R^1 st
( O is open & NAT c= O & A = (O \ NAT) \/ {REAL} ) ) ::_thesis: ( ex O being Subset of R^1 st
( O is open & NAT c= O & A = (O \ NAT) \/ {REAL} ) implies ( A is open & REAL in A ) )
proof
assume that
A3: A is open and
A4: REAL in A ; ::_thesis: ex O being Subset of R^1 st
( O is open & NAT c= O & A = (O \ NAT) \/ {REAL} )
consider O being Subset of R^1 such that
A5: O = (f " (A `)) ` ;
A ` is closed by A3, TOPS_1:4;
then f " (A `) is closed by A2;
then A6: (f " (A `)) ` is open by TOPS_1:3;
A7: not REAL in ([#] REAL?) \ A by A4, XBOOLE_0:def_5;
A8: A ` c= (A `) \ {REAL}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A ` or x in (A `) \ {REAL} )
assume A9: x in A ` ; ::_thesis: x in (A `) \ {REAL}
then not x in {REAL} by A7, TARSKI:def_1;
hence x in (A `) \ {REAL} by A9, XBOOLE_0:def_5; ::_thesis: verum
end;
A ` c= the carrier of REAL? ;
then A10: A ` c= (REAL \ NAT) \/ {REAL} by Def8;
A11: A ` c= REAL \ NAT
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A ` or x in REAL \ NAT )
assume A12: x in A ` ; ::_thesis: x in REAL \ NAT
then ( x in REAL \ NAT or x in {REAL} ) by A10, XBOOLE_0:def_3;
hence x in REAL \ NAT by A7, A12, TARSKI:def_1; ::_thesis: verum
end;
(A `) \ {REAL} c= A ` by XBOOLE_1:36;
then A13: A ` = (A `) \ {REAL} by A8, XBOOLE_0:def_10;
not REAL in REAL ;
then ((id REAL) +* (NAT --> REAL)) " ((A `) \ {REAL}) = (A `) \ NAT by A11, Th19, XBOOLE_1:1;
then O = (([#] R^1) \ (A `)) \/ (NAT /\ ([#] R^1)) by A1, A5, A13, XBOOLE_1:52;
then A14: O = (([#] R^1) \ (A `)) \/ NAT by TOPMETR:17, XBOOLE_1:28;
A = (A `) `
.= the carrier of REAL? \ (A `) ;
then A15: A = ((REAL \ NAT) \/ {REAL}) \ (A `) by Def8;
A16: A = ((REAL \ (A `)) \ NAT) \/ {REAL}
proof
thus A c= ((REAL \ (A `)) \ NAT) \/ {REAL} :: according to XBOOLE_0:def_10 ::_thesis: ((REAL \ (A `)) \ NAT) \/ {REAL} c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in ((REAL \ (A `)) \ NAT) \/ {REAL} )
assume A17: x in A ; ::_thesis: x in ((REAL \ (A `)) \ NAT) \/ {REAL}
then A18: not x in A ` by XBOOLE_0:def_5;
( x in REAL \ NAT or x in {REAL} ) by A15, A17, XBOOLE_0:def_3;
then ( ( x in REAL \ (A `) & not x in NAT ) or x in {REAL} ) by A18, XBOOLE_0:def_5;
then ( x in (REAL \ (A `)) \ NAT or x in {REAL} ) by XBOOLE_0:def_5;
hence x in ((REAL \ (A `)) \ NAT) \/ {REAL} by XBOOLE_0:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((REAL \ (A `)) \ NAT) \/ {REAL} or x in A )
assume x in ((REAL \ (A `)) \ NAT) \/ {REAL} ; ::_thesis: x in A
then ( x in (REAL \ (A `)) \ NAT or x in {REAL} ) by XBOOLE_0:def_3;
then A19: ( ( x in REAL \ (A `) & not x in NAT ) or ( x in {REAL} & not x in A ` ) ) by A7, TARSKI:def_1, XBOOLE_0:def_5;
then ( x in REAL \ NAT or x in {REAL} ) by XBOOLE_0:def_5;
then A20: x in (REAL \ NAT) \/ {REAL} by XBOOLE_0:def_3;
not x in A ` by A19, XBOOLE_0:def_5;
hence x in A by A15, A20, XBOOLE_0:def_5; ::_thesis: verum
end;
NAT c= REAL \ (A `)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in NAT or x in REAL \ (A `) )
assume A21: x in NAT ; ::_thesis: x in REAL \ (A `)
then not x in A ` by A11, XBOOLE_0:def_5;
hence x in REAL \ (A `) by A21, XBOOLE_0:def_5; ::_thesis: verum
end;
then O = REAL \ (A `) by A14, TOPMETR:17, XBOOLE_1:12;
hence ex O being Subset of R^1 st
( O is open & NAT c= O & A = (O \ NAT) \/ {REAL} ) by A5, A6, A14, A16, XBOOLE_1:7; ::_thesis: verum
end;
given O being Subset of R^1 such that A22: O is open and
A23: NAT c= O and
A24: A = (O \ NAT) \/ {REAL} ; ::_thesis: ( A is open & REAL in A )
consider B being Subset of R^1 such that
A25: B = ([#] R^1) \ O ;
not REAL in REAL ;
then ((id REAL) +* (NAT --> REAL)) " ((REAL \ O) \ {REAL}) = (REAL \ O) \ NAT by Th19;
then A26: f " ((REAL \ O) \ {REAL}) = REAL \ (O \/ NAT) by A1, XBOOLE_1:41;
A27: B is closed by A22, A25, Lm2;
A ` = ((REAL \ NAT) \/ {REAL}) \ ((O \ NAT) \/ {REAL}) by A24, Def8
.= ((REAL \ NAT) \ ((O \ NAT) \/ {REAL})) \/ ({REAL} \ ({REAL} \/ (O \ NAT))) by XBOOLE_1:42
.= ((REAL \ NAT) \ ((O \ NAT) \/ {REAL})) \/ {} by XBOOLE_1:46
.= ((REAL \ NAT) \ (O \ NAT)) \ {REAL} by XBOOLE_1:41
.= (REAL \ (NAT \/ (O \ NAT))) \ {REAL} by XBOOLE_1:41
.= (REAL \ (NAT \/ O)) \ {REAL} by XBOOLE_1:39
.= (REAL \ O) \ {REAL} by A23, XBOOLE_1:12 ;
then f " (A `) = B by A23, A25, A26, TOPMETR:17, XBOOLE_1:12;
then ([#] REAL?) \ A is closed by A2, A27;
hence A is open by Lm2; ::_thesis: REAL in A
REAL in {REAL} by TARSKI:def_1;
hence REAL in A by A24, XBOOLE_0:def_3; ::_thesis: verum
end;
theorem Th29: :: FRECHET:29
for A being set holds
( A is Subset of REAL? & not REAL in A iff ( A is Subset of R^1 & NAT /\ A = {} ) )
proof
let A be set ; ::_thesis: ( A is Subset of REAL? & not REAL in A iff ( A is Subset of R^1 & NAT /\ A = {} ) )
thus ( A is Subset of REAL? & not REAL in A implies ( A is Subset of R^1 & NAT /\ A = {} ) ) ::_thesis: ( A is Subset of R^1 & NAT /\ A = {} implies ( A is Subset of REAL? & not REAL in A ) )
proof
assume that
A1: A is Subset of REAL? and
A2: not REAL in A ; ::_thesis: ( A is Subset of R^1 & NAT /\ A = {} )
A c= the carrier of REAL? by A1;
then A3: A c= (REAL \ NAT) \/ {REAL} by Def8;
A c= REAL
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in REAL )
assume A4: x in A ; ::_thesis: x in REAL
then ( x in REAL \ NAT or x in {REAL} ) by A3, XBOOLE_0:def_3;
hence x in REAL by A2, A4, TARSKI:def_1; ::_thesis: verum
end;
hence A is Subset of R^1 by TOPMETR:17; ::_thesis: NAT /\ A = {}
thus NAT /\ A = {} ::_thesis: verum
proof
set x = the Element of NAT /\ A;
assume A5: NAT /\ A <> {} ; ::_thesis: contradiction
then A6: the Element of NAT /\ A in NAT by XBOOLE_0:def_4;
A7: the Element of NAT /\ A in A by A5, XBOOLE_0:def_4;
percases ( the Element of NAT /\ A in REAL \ NAT or the Element of NAT /\ A in {REAL} ) by A3, A7, XBOOLE_0:def_3;
suppose the Element of NAT /\ A in REAL \ NAT ; ::_thesis: contradiction
hence contradiction by A6, XBOOLE_0:def_5; ::_thesis: verum
end;
suppose the Element of NAT /\ A in {REAL} ; ::_thesis: contradiction
then the Element of NAT /\ A = REAL by TARSKI:def_1;
then REAL in REAL by A6;
hence contradiction ; ::_thesis: verum
end;
end;
end;
end;
assume that
A8: A is Subset of R^1 and
A9: NAT /\ A = {} ; ::_thesis: ( A is Subset of REAL? & not REAL in A )
A10: A c= REAL \ NAT
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in REAL \ NAT )
assume A11: x in A ; ::_thesis: x in REAL \ NAT
then not x in NAT by A9, XBOOLE_0:def_4;
hence x in REAL \ NAT by A8, A11, TOPMETR:17, XBOOLE_0:def_5; ::_thesis: verum
end;
REAL \ NAT c= (REAL \ NAT) \/ {REAL} by XBOOLE_1:7;
then A c= (REAL \ NAT) \/ {REAL} by A10, XBOOLE_1:1;
hence A is Subset of REAL? by Def8; ::_thesis: not REAL in A
thus not REAL in A ::_thesis: verum
proof
assume REAL in A ; ::_thesis: contradiction
then REAL in REAL by A8, TOPMETR:17;
hence contradiction ; ::_thesis: verum
end;
end;
theorem Th30: :: FRECHET:30
for A being Subset of R^1
for B being Subset of REAL? st A = B holds
( NAT /\ A = {} & A is open iff ( not REAL in B & B is open ) )
proof
let A be Subset of R^1; ::_thesis: for B being Subset of REAL? st A = B holds
( NAT /\ A = {} & A is open iff ( not REAL in B & B is open ) )
let B be Subset of REAL?; ::_thesis: ( A = B implies ( NAT /\ A = {} & A is open iff ( not REAL in B & B is open ) ) )
consider f being Function of R^1,REAL? such that
A1: f = (id REAL) +* (NAT --> REAL) and
A2: for A being Subset of REAL? holds
( A is closed iff f " A is closed ) by Def8;
assume A3: A = B ; ::_thesis: ( NAT /\ A = {} & A is open iff ( not REAL in B & B is open ) )
A4: ( NAT /\ A = {} & not REAL in B implies f " (B `) = A ` )
proof
assume that
A5: NAT /\ A = {} and
A6: not REAL in B ; ::_thesis: f " (B `) = A `
A7: REAL \ A = ((((REAL \ NAT) \/ {REAL}) \ A) \ {REAL}) \/ NAT
proof
thus REAL \ A c= ((((REAL \ NAT) \/ {REAL}) \ A) \ {REAL}) \/ NAT :: according to XBOOLE_0:def_10 ::_thesis: ((((REAL \ NAT) \/ {REAL}) \ A) \ {REAL}) \/ NAT c= REAL \ A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in REAL \ A or x in ((((REAL \ NAT) \/ {REAL}) \ A) \ {REAL}) \/ NAT )
assume A8: x in REAL \ A ; ::_thesis: x in ((((REAL \ NAT) \/ {REAL}) \ A) \ {REAL}) \/ NAT
then A9: not x in A by XBOOLE_0:def_5;
A10: x in REAL by A8;
A11: not x in {REAL}
proof
assume x in {REAL} ; ::_thesis: contradiction
then x = REAL by TARSKI:def_1;
hence contradiction by A10; ::_thesis: verum
end;
percases ( x in NAT or not x in NAT ) ;
suppose x in NAT ; ::_thesis: x in ((((REAL \ NAT) \/ {REAL}) \ A) \ {REAL}) \/ NAT
hence x in ((((REAL \ NAT) \/ {REAL}) \ A) \ {REAL}) \/ NAT by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose not x in NAT ; ::_thesis: x in ((((REAL \ NAT) \/ {REAL}) \ A) \ {REAL}) \/ NAT
then x in REAL \ NAT by A8, XBOOLE_0:def_5;
then x in (REAL \ NAT) \/ {REAL} by XBOOLE_0:def_3;
then x in ((REAL \ NAT) \/ {REAL}) \ A by A9, XBOOLE_0:def_5;
then x in (((REAL \ NAT) \/ {REAL}) \ A) \ {REAL} by A11, XBOOLE_0:def_5;
hence x in ((((REAL \ NAT) \/ {REAL}) \ A) \ {REAL}) \/ NAT by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((((REAL \ NAT) \/ {REAL}) \ A) \ {REAL}) \/ NAT or x in REAL \ A )
assume A12: x in ((((REAL \ NAT) \/ {REAL}) \ A) \ {REAL}) \/ NAT ; ::_thesis: x in REAL \ A
percases ( x in NAT or x in (((REAL \ NAT) \/ {REAL}) \ A) \ {REAL} ) by A12, XBOOLE_0:def_3;
supposeA13: x in NAT ; ::_thesis: x in REAL \ A
then not x in A by A5, XBOOLE_0:def_4;
hence x in REAL \ A by A13, XBOOLE_0:def_5; ::_thesis: verum
end;
supposeA14: x in (((REAL \ NAT) \/ {REAL}) \ A) \ {REAL} ; ::_thesis: x in REAL \ A
then x in ((REAL \ NAT) \/ {REAL}) \ A by XBOOLE_0:def_5;
then A15: not x in A by XBOOLE_0:def_5;
( x in REAL \ NAT or x in {REAL} ) by A14, XBOOLE_0:def_3;
hence x in REAL \ A by A14, A15, XBOOLE_0:def_5; ::_thesis: verum
end;
end;
end;
B ` c= the carrier of REAL? ;
then A16: B ` c= (REAL \ NAT) \/ {REAL} by Def8;
A17: (B `) \ {REAL} c= REAL
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (B `) \ {REAL} or x in REAL )
assume A18: x in (B `) \ {REAL} ; ::_thesis: x in REAL
then x in B ` by XBOOLE_0:def_5;
then ( x in REAL \ NAT or x in {REAL} ) by A16, XBOOLE_0:def_3;
hence x in REAL by A18, XBOOLE_0:def_5; ::_thesis: verum
end;
A19: REAL in ([#] REAL?) \ B by A6, Th27, XBOOLE_0:def_5;
{REAL} c= B `
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {REAL} or x in B ` )
assume x in {REAL} ; ::_thesis: x in B `
hence x in B ` by A19, TARSKI:def_1; ::_thesis: verum
end;
then ( not REAL in REAL & B ` = ((B `) \ {REAL}) \/ {REAL} ) by XBOOLE_1:45;
then ((id REAL) +* (NAT --> REAL)) " (B `) = ((([#] REAL?) \ B) \ {REAL}) \/ NAT by A17, Th18
.= ((((REAL \ NAT) \/ {REAL}) \ A) \ {REAL}) \/ NAT by A3, Def8 ;
hence f " (B `) = A ` by A1, A7, TOPMETR:17; ::_thesis: verum
end;
thus ( NAT /\ A = {} & A is open implies ( not REAL in B & B is open ) ) ::_thesis: ( not REAL in B & B is open implies ( NAT /\ A = {} & A is open ) )
proof
assume that
A20: NAT /\ A = {} and
A21: A is open ; ::_thesis: ( not REAL in B & B is open )
thus not REAL in B by A3, A20, Th29; ::_thesis: B is open
A ` is closed by A21, TOPS_1:4;
then B ` is closed by A3, A2, A4, A20, Th29;
hence B is open by TOPS_1:4; ::_thesis: verum
end;
assume that
A22: not REAL in B and
A23: B is open ; ::_thesis: ( NAT /\ A = {} & A is open )
thus NAT /\ A = {} by A3, A22, Th29; ::_thesis: A is open
B ` is closed by A23, TOPS_1:4;
then A ` is closed by A3, A2, A4, A22, Th29;
hence A is open by TOPS_1:4; ::_thesis: verum
end;
theorem Th31: :: FRECHET:31
for A being Subset of REAL? st A = {REAL} holds
A is closed
proof
reconsider B = REAL \ NAT as Subset of R^1 by TOPMETR:17;
let A be Subset of REAL?; ::_thesis: ( A = {REAL} implies A is closed )
reconsider B = B as Subset of R^1 ;
A1: REAL \ NAT = ((REAL \ NAT) \/ {REAL}) \ {REAL}
proof
thus REAL \ NAT c= ((REAL \ NAT) \/ {REAL}) \ {REAL} :: according to XBOOLE_0:def_10 ::_thesis: ((REAL \ NAT) \/ {REAL}) \ {REAL} c= REAL \ NAT
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in REAL \ NAT or x in ((REAL \ NAT) \/ {REAL}) \ {REAL} )
assume A2: x in REAL \ NAT ; ::_thesis: x in ((REAL \ NAT) \/ {REAL}) \ {REAL}
then A3: x in REAL ;
A4: not x in {REAL}
proof
assume x in {REAL} ; ::_thesis: contradiction
then x = REAL by TARSKI:def_1;
hence contradiction by A3; ::_thesis: verum
end;
x in (REAL \ NAT) \/ {REAL} by A2, XBOOLE_0:def_3;
hence x in ((REAL \ NAT) \/ {REAL}) \ {REAL} by A4, XBOOLE_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((REAL \ NAT) \/ {REAL}) \ {REAL} or x in REAL \ NAT )
assume A5: x in ((REAL \ NAT) \/ {REAL}) \ {REAL} ; ::_thesis: x in REAL \ NAT
then not x in {REAL} by XBOOLE_0:def_5;
hence x in REAL \ NAT by A5, XBOOLE_0:def_3; ::_thesis: verum
end;
B misses NAT by XBOOLE_1:79;
then A6: B /\ NAT = {} by XBOOLE_0:def_7;
then reconsider C = B as Subset of REAL? by Th29;
assume A = {REAL} ; ::_thesis: A is closed
then A7: C = A ` by A1, Def8;
B is open
proof
reconsider N = NAT as Subset of R^1 by TOPMETR:17;
reconsider N = N as Subset of R^1 ;
( N is closed & N ` = B ) by Th10, TOPMETR:17;
hence B is open by TOPS_1:3; ::_thesis: verum
end;
then C is open by A6, Th30;
hence A is closed by A7, TOPS_1:3; ::_thesis: verum
end;
theorem Th32: :: FRECHET:32
not REAL? is first-countable
proof
reconsider y = REAL as Point of REAL? by Th27;
assume REAL? is first-countable ; ::_thesis: contradiction
then consider B being Basis of y such that
A1: B is countable by Def2;
consider h being Function of NAT,B such that
A2: rng h = B by A1, CARD_3:96;
defpred S1[ set , set ] means ex m being Element of NAT st
( m = $1 & $2 in (h . $1) /\ ].(m - (1 / 4)),(m + (1 / 4)).[ );
A3: for n being set st n in NAT holds
ex x being set st
( x in REAL \ NAT & S1[n,x] )
proof
let n be set ; ::_thesis: ( n in NAT implies ex x being set st
( x in REAL \ NAT & S1[n,x] ) )
assume A4: n in NAT ; ::_thesis: ex x being set st
( x in REAL \ NAT & S1[n,x] )
then reconsider m = n as Element of NAT ;
n in dom h by A4, FUNCT_2:def_1;
then A5: h . n in rng h by FUNCT_1:def_3;
then reconsider Bn = h . n as Subset of REAL? by A2;
reconsider m9 = m as Point of RealSpace by METRIC_1:def_13;
reconsider Kn = Ball (m9,(1 / 4)) as Subset of R^1 by TOPMETR:12;
reconsider Bn = Bn as Subset of REAL? ;
( Bn is open & y in Bn ) by A5, YELLOW_8:12;
then consider An being Subset of R^1 such that
A6: An is open and
A7: NAT c= An and
A8: Bn = (An \ NAT) \/ {REAL} by Th28;
reconsider An9 = An as Subset of R^1 ;
Kn is open by TOPMETR:14;
then A9: An9 /\ Kn is open by A6, TOPS_1:11;
dist (m9,m9) = 0 by METRIC_1:1;
then m9 in Ball (m9,(1 / 4)) by METRIC_1:11;
then n in An /\ (Ball (m9,(1 / 4))) by A4, A7, XBOOLE_0:def_4;
then consider r being real number such that
A10: r > 0 and
A11: Ball (m9,r) c= An /\ Kn by A9, TOPMETR:15;
reconsider r = r as Real by XREAL_0:def_1;
m < m + r by A10, XREAL_1:29;
then m - r < m by XREAL_1:19;
then consider x being real number such that
A12: m - r < x and
A13: x < m by XREAL_1:5;
reconsider x = x as Real by XREAL_0:def_1;
take x ; ::_thesis: ( x in REAL \ NAT & S1[n,x] )
A14: r < 1
proof
assume r >= 1 ; ::_thesis: contradiction
then 1 / 2 < r by XXREAL_0:2;
then - r < - (1 / 2) by XREAL_1:24;
then A15: (- r) + m < (- (1 / 2)) + m by XREAL_1:6;
(- (1 / 2)) + m < r + m by A10, XREAL_1:6;
then m - (1 / 2) in { a where a is Real : ( m - r < a & a < m + r ) } by A15;
then m - (1 / 2) in ].(m - r),(m + r).[ by RCOMP_1:def_2;
then m - (1 / 2) in Ball (m9,r) by Th7;
then m - (1 / 2) in Kn by A11, XBOOLE_0:def_4;
then m - (1 / 2) in ].(m - (1 / 4)),(m + (1 / 4)).[ by Th7;
then m - (1 / 2) in { a where a is Real : ( m - (1 / 4) < a & a < m + (1 / 4) ) } by RCOMP_1:def_2;
then ex a being Real st
( a = m - (1 / 2) & m - (1 / 4) < a & a < m + (1 / 4) ) ;
hence contradiction by XREAL_1:6; ::_thesis: verum
end;
A16: not x in NAT
proof
assume x in NAT ; ::_thesis: contradiction
then reconsider x = x as Element of NAT ;
percases ( x = m or x > m or x < m ) by XXREAL_0:1;
suppose x = m ; ::_thesis: contradiction
hence contradiction by A13; ::_thesis: verum
end;
suppose x > m ; ::_thesis: contradiction
hence contradiction by A13; ::_thesis: verum
end;
supposeA17: x < m ; ::_thesis: contradiction
m < x + r by A12, XREAL_1:19;
then m - x < r by XREAL_1:19;
then A18: m - x < 1 by A14, XXREAL_0:2;
m >= x + 1 by A17, NAT_1:13;
hence contradiction by A18, XREAL_1:19; ::_thesis: verum
end;
end;
end;
hence x in REAL \ NAT by XBOOLE_0:def_5; ::_thesis: S1[n,x]
x + 0 < m + r by A10, A13, XREAL_1:8;
then x in { a where a is Real : ( m - r < a & a < m + r ) } by A12;
then x in ].(m - r),(m + r).[ by RCOMP_1:def_2;
then A19: x in Ball (m9,r) by Th7;
then x in An by A11, XBOOLE_0:def_4;
then x in An \ NAT by A16, XBOOLE_0:def_5;
then A20: x in Bn by A8, XBOOLE_0:def_3;
take m ; ::_thesis: ( m = n & x in (h . n) /\ ].(m - (1 / 4)),(m + (1 / 4)).[ )
Ball (m9,(1 / 4)) = ].(m - (1 / 4)),(m + (1 / 4)).[ by Th7;
then x in ].(m - (1 / 4)),(m + (1 / 4)).[ by A11, A19, XBOOLE_0:def_4;
hence ( m = n & x in (h . n) /\ ].(m - (1 / 4)),(m + (1 / 4)).[ ) by A20, XBOOLE_0:def_4; ::_thesis: verum
end;
consider S being Function such that
A21: dom S = NAT and
A22: rng S c= REAL \ NAT and
A23: for n being set st n in NAT holds
S1[n,S . n] from FUNCT_1:sch_5(A3);
reconsider S = S as sequence of R^1 by A21, A22, FUNCT_2:2, TOPMETR:17, XBOOLE_1:1;
reconsider O = rng S as Subset of R^1 ;
for n being Element of NAT holds S . n in ].(n - (1 / 4)),(n + (1 / 4)).[
proof
let n be Element of NAT ; ::_thesis: S . n in ].(n - (1 / 4)),(n + (1 / 4)).[
ex m being Element of NAT st
( m = n & S . n in (h . n) /\ ].(m - (1 / 4)),(m + (1 / 4)).[ ) by A23;
hence S . n in ].(n - (1 / 4)),(n + (1 / 4)).[ by XBOOLE_0:def_4; ::_thesis: verum
end;
then O is closed by Th9;
then A24: ([#] R^1) \ O is open by PRE_TOPC:def_3;
set A = ((O `) \ NAT) \/ {REAL};
((O `) \ NAT) \/ {REAL} c= (REAL \ NAT) \/ {REAL}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((O `) \ NAT) \/ {REAL} or x in (REAL \ NAT) \/ {REAL} )
assume x in ((O `) \ NAT) \/ {REAL} ; ::_thesis: x in (REAL \ NAT) \/ {REAL}
then ( x in (O `) \ NAT or x in {REAL} ) by XBOOLE_0:def_3;
then ( ( x in O ` & not x in NAT ) or x in {REAL} ) by XBOOLE_0:def_5;
then ( x in REAL \ NAT or x in {REAL} ) by TOPMETR:17, XBOOLE_0:def_5;
hence x in (REAL \ NAT) \/ {REAL} by XBOOLE_0:def_3; ::_thesis: verum
end;
then reconsider A = ((O `) \ NAT) \/ {REAL} as Subset of REAL? by Def8;
reconsider A = A as Subset of REAL? ;
NAT c= O `
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in NAT or x in O ` )
assume A25: x in NAT ; ::_thesis: x in O `
then not x in rng S by A22, XBOOLE_0:def_5;
hence x in O ` by A25, TOPMETR:17, XBOOLE_0:def_5; ::_thesis: verum
end;
then ( A is open & REAL in A ) by A24, Th28;
then consider V being Subset of REAL? such that
A26: V in B and
A27: V c= A by YELLOW_8:13;
consider n1 being set such that
A28: n1 in dom h and
A29: V = h . n1 by A2, A26, FUNCT_1:def_3;
reconsider n = n1 as Element of NAT by A28;
for n being Element of NAT ex x being set st
( x in h . n & not x in A )
proof
let n be Element of NAT ; ::_thesis: ex x being set st
( x in h . n & not x in A )
consider xn being set such that
A30: xn = S . n ;
take xn ; ::_thesis: ( xn in h . n & not xn in A )
A31: S . n in rng S by A21, FUNCT_1:def_3;
then not xn in ([#] R^1) \ O by A30, XBOOLE_0:def_5;
then A32: not xn in (O `) \ NAT by XBOOLE_0:def_5;
not xn = REAL
proof
assume xn = REAL ; ::_thesis: contradiction
then REAL in REAL by A22, A30, A31, XBOOLE_0:def_5;
hence contradiction ; ::_thesis: verum
end;
then A33: not xn in {REAL} by TARSKI:def_1;
ex m being Element of NAT st
( m = n & S . n in (h . n) /\ ].(m - (1 / 4)),(m + (1 / 4)).[ ) by A23;
hence ( xn in h . n & not xn in A ) by A30, A32, A33, XBOOLE_0:def_3, XBOOLE_0:def_4; ::_thesis: verum
end;
then ex x being set st
( x in h . n & not x in A ) ;
hence contradiction by A27, A29; ::_thesis: verum
end;
theorem Th33: :: FRECHET:33
REAL? is Frechet
proof
let A be Subset of REAL?; :: according to FRECHET:def_6 ::_thesis: for x being Point of REAL? st x in Cl A holds
ex S being sequence of REAL? st
( rng S c= A & x in Lim S )
let x be Point of REAL?; ::_thesis: ( x in Cl A implies ex S being sequence of REAL? st
( rng S c= A & x in Lim S ) )
assume A1: x in Cl A ; ::_thesis: ex S being sequence of REAL? st
( rng S c= A & x in Lim S )
x in the carrier of REAL? ;
then x in (REAL \ NAT) \/ {REAL} by Def8;
then A2: ( x in REAL \ NAT or x in {REAL} ) by XBOOLE_0:def_3;
percases ( x in REAL \ NAT or ( x = REAL & x in A ) or ( x = REAL & not x in A ) ) by A2, TARSKI:def_1;
supposeA3: x in REAL \ NAT ; ::_thesis: ex S being sequence of REAL? st
( rng S c= A & x in Lim S )
then A4: x in REAL ;
A c= the carrier of REAL? ;
then A5: A c= (REAL \ NAT) \/ {REAL} by Def8;
A \ {REAL} c= REAL
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A \ {REAL} or a in REAL )
assume A6: a in A \ {REAL} ; ::_thesis: a in REAL
then a in A by XBOOLE_0:def_5;
then ( a in REAL \ NAT or a in {REAL} ) by A5, XBOOLE_0:def_3;
hence a in REAL by A6, XBOOLE_0:def_5; ::_thesis: verum
end;
then reconsider A9 = A \ {REAL} as Subset of R^1 by TOPMETR:17;
reconsider x9 = x as Point of R^1 by A3, TOPMETR:17;
reconsider A9 = A9 as Subset of R^1 ;
for B9 being Subset of R^1 st B9 is open & x9 in B9 holds
A9 meets B9
proof
reconsider C = NAT as Subset of R^1 by TOPMETR:17;
let B9 be Subset of R^1; ::_thesis: ( B9 is open & x9 in B9 implies A9 meets B9 )
reconsider B1 = B9 as Subset of R^1 ;
reconsider C = C as Subset of R^1 ;
A7: not x9 in NAT by A3, XBOOLE_0:def_5;
B9 \ NAT misses NAT by XBOOLE_1:79;
then A8: (B9 \ NAT) /\ NAT = {} by XBOOLE_0:def_7;
then reconsider D = B1 \ C as Subset of REAL? by Th29;
assume B9 is open ; ::_thesis: ( not x9 in B9 or A9 meets B9 )
then B1 \ C is open by Th4, Th10;
then A9: D is open by A8, Th30;
reconsider D = D as Subset of REAL? ;
assume x9 in B9 ; ::_thesis: A9 meets B9
then x9 in B9 \ NAT by A7, XBOOLE_0:def_5;
then A meets D by A1, A9, PRE_TOPC:def_7;
then A10: A /\ D <> {} by XBOOLE_0:def_7;
A9 /\ B9 <> {}
proof
set a = the Element of A /\ D;
A11: the Element of A /\ D in D by A10, XBOOLE_0:def_4;
then A12: the Element of A /\ D in B9 by XBOOLE_0:def_5;
A13: the Element of A /\ D in REAL by A11, TOPMETR:17;
A14: not the Element of A /\ D in {REAL}
proof
assume the Element of A /\ D in {REAL} ; ::_thesis: contradiction
then the Element of A /\ D = REAL by TARSKI:def_1;
hence contradiction by A13; ::_thesis: verum
end;
the Element of A /\ D in A by A10, XBOOLE_0:def_4;
then the Element of A /\ D in A \ {REAL} by A14, XBOOLE_0:def_5;
hence A9 /\ B9 <> {} by A12, XBOOLE_0:def_4; ::_thesis: verum
end;
hence A9 meets B9 by XBOOLE_0:def_7; ::_thesis: verum
end;
then x9 in Cl A9 by PRE_TOPC:def_7;
then consider S9 being sequence of R^1 such that
A15: rng S9 c= A9 and
A16: x9 in Lim S9 by Def6;
A17: rng S9 c= A
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng S9 or a in A )
assume a in rng S9 ; ::_thesis: a in A
hence a in A by A15, XBOOLE_0:def_5; ::_thesis: verum
end;
then reconsider S = S9 as sequence of REAL? by Th2, XBOOLE_1:1;
take S ; ::_thesis: ( rng S c= A & x in Lim S )
thus rng S c= A by A17; ::_thesis: x in Lim S
A18: S9 is_convergent_to x9 by A16, Def5;
S is_convergent_to x
proof
reconsider C = {REAL} as Subset of REAL? by Lm3;
let V be Subset of REAL?; :: according to FRECHET:def_3 ::_thesis: ( V is open & x in V implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
S . m in V )
assume that
A19: V is open and
A20: x in V ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
S . m in V
reconsider C = C as Subset of REAL? ;
REAL in {REAL} by TARSKI:def_1;
then A21: not REAL in V \ {REAL} by XBOOLE_0:def_5;
then reconsider V9 = V \ C as Subset of R^1 by Th29;
V \ C is open by A19, Th4, Th31;
then A22: V9 is open by A21, Th30;
not x in C
proof
assume x in C ; ::_thesis: contradiction
then x = REAL by TARSKI:def_1;
hence contradiction by A4; ::_thesis: verum
end;
then x in V \ C by A20, XBOOLE_0:def_5;
then consider n being Element of NAT such that
A23: for m being Element of NAT st n <= m holds
S9 . m in V9 by A18, A22, Def3;
take n ; ::_thesis: for m being Element of NAT st n <= m holds
S . m in V
thus for m being Element of NAT st n <= m holds
S . m in V ::_thesis: verum
proof
let m be Element of NAT ; ::_thesis: ( n <= m implies S . m in V )
assume n <= m ; ::_thesis: S . m in V
then S9 . m in V9 by A23;
hence S . m in V by XBOOLE_0:def_5; ::_thesis: verum
end;
end;
hence x in Lim S by Def5; ::_thesis: verum
end;
supposeA24: ( x = REAL & x in A ) ; ::_thesis: ex S being sequence of REAL? st
( rng S c= A & x in Lim S )
reconsider S = NAT --> x as sequence of REAL? ;
take S ; ::_thesis: ( rng S c= A & x in Lim S )
{x} c= A by A24, ZFMISC_1:31;
hence rng S c= A by FUNCOP_1:8; ::_thesis: x in Lim S
S is_convergent_to x by Th22;
hence x in Lim S by Def5; ::_thesis: verum
end;
supposeA25: ( x = REAL & not x in A ) ; ::_thesis: ex S being sequence of REAL? st
( rng S c= A & x in Lim S )
then reconsider A9 = A as Subset of R^1 by Th29;
ex k being Point of R^1 st
( k in NAT & ex S9 being sequence of R^1 st
( rng S9 c= A9 & S9 is_convergent_to k ) )
proof
defpred S1[ set , set ] means ( $1 in $2 & $2 in the topology of R^1 & $2 /\ A9 = {} );
assume A26: for k being Point of R^1 holds
( not k in NAT or for S9 being sequence of R^1 holds
( not rng S9 c= A9 or not S9 is_convergent_to k ) ) ; ::_thesis: contradiction
A27: for k being set st k in NAT holds
ex U1 being set st S1[k,U1]
proof
given k being set such that A28: k in NAT and
A29: for U1 being set st k in U1 & U1 in the topology of R^1 holds
not U1 /\ A9 = {} ; ::_thesis: contradiction
reconsider k = k as Point of R^1 by A28, TOPMETR:17;
reconsider k99 = k as Point of (TopSpaceMetr RealSpace) ;
reconsider k9 = k99 as Point of RealSpace by TOPMETR:12;
set Bs = Balls k99;
consider h being Function of NAT,(Balls k99) such that
A30: for n being Element of NAT holds h . n = Ball (k9,(1 / (n + 1))) by Th11;
defpred S2[ set , set ] means $2 in (h . $1) /\ A9;
A31: for n being set st n in NAT holds
ex z being set st
( z in the carrier of R^1 & S2[n,z] )
proof
let n be set ; ::_thesis: ( n in NAT implies ex z being set st
( z in the carrier of R^1 & S2[n,z] ) )
assume n in NAT ; ::_thesis: ex z being set st
( z in the carrier of R^1 & S2[n,z] )
then reconsider n = n as Element of NAT ;
A32: h . n in Balls k99 ;
then reconsider H = h . n as Subset of R^1 ;
take z = the Element of H /\ A9; ::_thesis: ( z in the carrier of R^1 & S2[n,z] )
Balls k99 c= the topology of R^1 by TOPS_2:64;
then A33: H /\ A9 <> {} by A29, A32, YELLOW_8:12;
then z in H by XBOOLE_0:def_4;
hence ( z in the carrier of R^1 & S2[n,z] ) by A33; ::_thesis: verum
end;
consider S9 being Function such that
A34: ( dom S9 = NAT & rng S9 c= the carrier of R^1 ) and
A35: for n being set st n in NAT holds
S2[n,S9 . n] from FUNCT_1:sch_5(A31);
reconsider S9 = S9 as Function of NAT, the carrier of R^1 by A34, FUNCT_2:2;
A36: S9 is_convergent_to k
proof
let U1 be Subset of R^1; :: according to FRECHET:def_3 ::_thesis: ( U1 is open & k in U1 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
S9 . m in U1 )
assume ( U1 is open & k in U1 ) ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
S9 . m in U1
then consider r being real number such that
A37: r > 0 and
A38: Ball (k9,r) c= U1 by TOPMETR:15;
reconsider r = r as Real by XREAL_0:def_1;
consider n being Element of NAT such that
A39: 1 / n < r and
A40: n > 0 by A37, Lm1;
take n ; ::_thesis: for m being Element of NAT st n <= m holds
S9 . m in U1
thus for m being Element of NAT st n <= m holds
S9 . m in U1 ::_thesis: verum
proof
let m be Element of NAT ; ::_thesis: ( n <= m implies S9 . m in U1 )
S9 . m in (h . m) /\ A9 by A35;
then A41: S9 . m in h . m by XBOOLE_0:def_4;
assume n <= m ; ::_thesis: S9 . m in U1
then n < m + 1 by NAT_1:13;
then 1 / (m + 1) < 1 / n by A40, XREAL_1:88;
then Ball (k9,(1 / (m + 1))) c= Ball (k9,r) by A39, PCOMPS_1:1, XXREAL_0:2;
then A42: Ball (k9,(1 / (m + 1))) c= U1 by A38, XBOOLE_1:1;
h . m = Ball (k9,(1 / (m + 1))) by A30;
hence S9 . m in U1 by A42, A41; ::_thesis: verum
end;
end;
rng S9 c= A9
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng S9 or z in A9 )
assume z in rng S9 ; ::_thesis: z in A9
then consider z9 being set such that
A43: z9 in dom S9 and
A44: z = S9 . z9 by FUNCT_1:def_3;
S9 . z9 in (h . z9) /\ A9 by A35, A43;
hence z in A9 by A44, XBOOLE_0:def_4; ::_thesis: verum
end;
hence contradiction by A26, A28, A36; ::_thesis: verum
end;
consider g being Function such that
A45: ( dom g = NAT & ( for k being set st k in NAT holds
S1[k,g . k] ) ) from CLASSES1:sch_1(A27);
rng g c= bool the carrier of R^1
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng g or z in bool the carrier of R^1 )
assume z in rng g ; ::_thesis: z in bool the carrier of R^1
then consider k being set such that
A46: k in dom g and
A47: z = g . k by FUNCT_1:def_3;
g . k in the topology of R^1 by A45, A46;
hence z in bool the carrier of R^1 by A47; ::_thesis: verum
end;
then reconsider F = rng g as Subset-Family of R^1 ;
F is open
proof
let O be Subset of R^1; :: according to TOPS_2:def_1 ::_thesis: ( not O in F or O is open )
assume O in F ; ::_thesis: O is open
then consider k being set such that
A48: k in dom g and
A49: O = g . k by FUNCT_1:def_3;
g . k in the topology of R^1 by A45, A48;
hence O is open by A49, PRE_TOPC:def_2; ::_thesis: verum
end;
then A50: union F is open by TOPS_2:19;
(union F) \ NAT c= REAL \ NAT by TOPMETR:17, XBOOLE_1:33;
then ((union F) \ NAT) \/ {REAL} c= (REAL \ NAT) \/ {REAL} by XBOOLE_1:9;
then reconsider B = ((union F) \ NAT) \/ {REAL} as Subset of REAL? by Def8;
reconsider B = B as Subset of REAL? ;
A51: B /\ A = {}
proof
set z = the Element of B /\ A;
assume A52: B /\ A <> {} ; ::_thesis: contradiction
then A53: the Element of B /\ A in B by XBOOLE_0:def_4;
A54: the Element of B /\ A in A by A52, XBOOLE_0:def_4;
percases ( the Element of B /\ A in (union F) \ NAT or the Element of B /\ A in {REAL} ) by A53, XBOOLE_0:def_3;
suppose the Element of B /\ A in (union F) \ NAT ; ::_thesis: contradiction
then the Element of B /\ A in union F by XBOOLE_0:def_5;
then consider C being set such that
A55: the Element of B /\ A in C and
A56: C in F by TARSKI:def_4;
consider l being set such that
A57: l in dom g and
A58: C = g . l by A56, FUNCT_1:def_3;
(g . l) /\ A = {} by A45, A57;
hence contradiction by A54, A55, A58, XBOOLE_0:def_4; ::_thesis: verum
end;
suppose the Element of B /\ A in {REAL} ; ::_thesis: contradiction
then the Element of B /\ A = REAL by TARSKI:def_1;
hence contradiction by A25, A52, XBOOLE_0:def_4; ::_thesis: verum
end;
end;
end;
NAT c= union F
proof
let k be set ; :: according to TARSKI:def_3 ::_thesis: ( not k in NAT or k in union F )
assume k in NAT ; ::_thesis: k in union F
then ( k in g . k & g . k in rng g ) by A45, FUNCT_1:def_3;
hence k in union F by TARSKI:def_4; ::_thesis: verum
end;
then ( B is open & REAL in B ) by A50, Th28;
then A meets B by A1, A25, PRE_TOPC:def_7;
hence contradiction by A51, XBOOLE_0:def_7; ::_thesis: verum
end;
then consider k being Point of R^1 such that
A59: k in NAT and
A60: ex S9 being sequence of R^1 st
( rng S9 c= A9 & S9 is_convergent_to k ) ;
consider S9 being sequence of R^1 such that
A61: rng S9 c= A9 and
A62: S9 is_convergent_to k by A60;
reconsider S = S9 as sequence of REAL? by A61, Th2, XBOOLE_1:1;
take S ; ::_thesis: ( rng S c= A & x in Lim S )
thus rng S c= A by A61; ::_thesis: x in Lim S
S is_convergent_to x
proof
let U1 be Subset of REAL?; :: according to FRECHET:def_3 ::_thesis: ( U1 is open & x in U1 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
S . m in U1 )
assume ( U1 is open & x in U1 ) ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
S . m in U1
then consider O being Subset of R^1 such that
A63: ( O is open & NAT c= O ) and
A64: U1 = (O \ NAT) \/ {REAL} by A25, Th28;
consider n being Element of NAT such that
A65: for m being Element of NAT st n <= m holds
S9 . m in O by A59, A62, A63, Def3;
take n ; ::_thesis: for m being Element of NAT st n <= m holds
S . m in U1
thus for m being Element of NAT st n <= m holds
S . m in U1 ::_thesis: verum
proof
let m be Element of NAT ; ::_thesis: ( n <= m implies S . m in U1 )
assume n <= m ; ::_thesis: S . m in U1
then A66: S9 . m in O by A65;
m in NAT ;
then m in dom S9 by NORMSP_1:12;
then S9 . m in rng S9 by FUNCT_1:def_3;
then S9 . m in A9 by A61;
then S9 . m in the carrier of REAL? ;
then S9 . m in (REAL \ NAT) \/ {REAL} by Def8;
then A67: ( S9 . m in REAL \ NAT or S9 . m in {REAL} ) by XBOOLE_0:def_3;
S9 . m <> REAL
proof
A68: S9 . m in REAL by TOPMETR:17;
assume S9 . m = REAL ; ::_thesis: contradiction
hence contradiction by A68; ::_thesis: verum
end;
then not S9 . m in NAT by A67, TARSKI:def_1, XBOOLE_0:def_5;
then S9 . m in O \ NAT by A66, XBOOLE_0:def_5;
hence S . m in U1 by A64, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
hence x in Lim S by Def5; ::_thesis: verum
end;
end;
end;
theorem :: FRECHET:34
ex T being non empty TopSpace st
( T is Frechet & not T is first-countable ) by Th32, Th33;
begin
theorem :: FRECHET:35
for f, g being Function st f tolerates g holds
rng (f +* g) = (rng f) \/ (rng g)
proof
let f, g be Function; ::_thesis: ( f tolerates g implies rng (f +* g) = (rng f) \/ (rng g) )
assume A1: f tolerates g ; ::_thesis: rng (f +* g) = (rng f) \/ (rng g)
thus rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17; :: according to XBOOLE_0:def_10 ::_thesis: (rng f) \/ (rng g) c= rng (f +* g)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (rng f) \/ (rng g) or x in rng (f +* g) )
assume A2: x in (rng f) \/ (rng g) ; ::_thesis: x in rng (f +* g)
A3: rng (f +* g) = (f .: ((dom f) \ (dom g))) \/ (rng g) by Th12;
A4: rng g c= rng (f +* g) by FUNCT_4:18;
percases ( x in rng g or not x in rng g ) ;
suppose x in rng g ; ::_thesis: x in rng (f +* g)
hence x in rng (f +* g) by A4; ::_thesis: verum
end;
supposeA5: not x in rng g ; ::_thesis: x in rng (f +* g)
then x in rng f by A2, XBOOLE_0:def_3;
then consider a being set such that
A6: a in dom f and
A7: x = f . a by FUNCT_1:def_3;
now__::_thesis:_not_a_in_dom_g
assume A8: a in dom g ; ::_thesis: contradiction
x = (f +* g) . a by A1, A6, A7, FUNCT_4:15
.= g . a by A8, FUNCT_4:13 ;
hence contradiction by A5, A8, FUNCT_1:def_3; ::_thesis: verum
end;
then a in (dom f) \ (dom g) by A6, XBOOLE_0:def_5;
then x in f .: ((dom f) \ (dom g)) by A7, FUNCT_1:def_6;
hence x in rng (f +* g) by A3, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
theorem :: FRECHET:36
for r being Real st r > 0 holds
ex n being Element of NAT st
( 1 / n < r & n > 0 ) by Lm1;