:: TOPS_2 semantic presentation
begin
theorem :: TOPS_2:1
for T being 1-sorted
for F being Subset-Family of T holds F c= bool ([#] T) ;
theorem Th2: :: TOPS_2:2
for T being 1-sorted
for F being Subset-Family of T
for X being set st X c= F holds
X is Subset-Family of T
proof
let T be 1-sorted ; ::_thesis: for F being Subset-Family of T
for X being set st X c= F holds
X is Subset-Family of T
let F be Subset-Family of T; ::_thesis: for X being set st X c= F holds
X is Subset-Family of T
let X be set ; ::_thesis: ( X c= F implies X is Subset-Family of T )
assume A1: X c= F ; ::_thesis: X is Subset-Family of T
X c= bool the carrier of T
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in X or y in bool the carrier of T )
assume y in X ; ::_thesis: y in bool the carrier of T
then y in F by A1;
hence y in bool the carrier of T ; ::_thesis: verum
end;
hence X is Subset-Family of T ; ::_thesis: verum
end;
theorem :: TOPS_2:3
for T being non empty 1-sorted
for F being Subset-Family of T st F is Cover of T holds
F <> {}
proof
let T be non empty 1-sorted ; ::_thesis: for F being Subset-Family of T st F is Cover of T holds
F <> {}
let F be Subset-Family of T; ::_thesis: ( F is Cover of T implies F <> {} )
set x = the Element of union F;
assume F is Cover of T ; ::_thesis: F <> {}
then union F = the carrier of T by SETFAM_1:45;
then ex A being set st
( the Element of union F in A & A in F ) by TARSKI:def_4;
hence F <> {} ; ::_thesis: verum
end;
theorem :: TOPS_2:4
for T being 1-sorted
for F, G being Subset-Family of T holds (union F) \ (union G) c= union (F \ G)
proof
let T be 1-sorted ; ::_thesis: for F, G being Subset-Family of T holds (union F) \ (union G) c= union (F \ G)
let F, G be Subset-Family of T; ::_thesis: (union F) \ (union G) c= union (F \ G)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (union F) \ (union G) or x in union (F \ G) )
assume A1: x in (union F) \ (union G) ; ::_thesis: x in union (F \ G)
then x in union F by XBOOLE_0:def_5;
then consider A being set such that
A2: x in A and
A3: A in F by TARSKI:def_4;
not x in union G by A1, XBOOLE_0:def_5;
then not A in G by A2, TARSKI:def_4;
then A in F \ G by A3, XBOOLE_0:def_5;
hence x in union (F \ G) by A2, TARSKI:def_4; ::_thesis: verum
end;
theorem :: TOPS_2:5
for T being set
for F being Subset-Family of T holds
( F <> {} iff COMPLEMENT F <> {} )
proof
let T be set ; ::_thesis: for F being Subset-Family of T holds
( F <> {} iff COMPLEMENT F <> {} )
let F be Subset-Family of T; ::_thesis: ( F <> {} iff COMPLEMENT F <> {} )
thus ( F <> {} implies COMPLEMENT F <> {} ) by SETFAM_1:32; ::_thesis: ( COMPLEMENT F <> {} implies F <> {} )
assume COMPLEMENT F <> {} ; ::_thesis: F <> {}
then COMPLEMENT (COMPLEMENT F) <> {} by SETFAM_1:32;
hence F <> {} ; ::_thesis: verum
end;
theorem Th6: :: TOPS_2:6
for T being set
for F being Subset-Family of T st F <> {} holds
meet (COMPLEMENT F) = (union F) `
proof
let T be set ; ::_thesis: for F being Subset-Family of T st F <> {} holds
meet (COMPLEMENT F) = (union F) `
let F be Subset-Family of T; ::_thesis: ( F <> {} implies meet (COMPLEMENT F) = (union F) ` )
assume F <> {} ; ::_thesis: meet (COMPLEMENT F) = (union F) `
then meet (COMPLEMENT F) = ([#] T) \ (union F) by SETFAM_1:33;
hence meet (COMPLEMENT F) = (union F) ` ; ::_thesis: verum
end;
theorem Th7: :: TOPS_2:7
for T being set
for F being Subset-Family of T st F <> {} holds
union (COMPLEMENT F) = (meet F) `
proof
let T be set ; ::_thesis: for F being Subset-Family of T st F <> {} holds
union (COMPLEMENT F) = (meet F) `
let F be Subset-Family of T; ::_thesis: ( F <> {} implies union (COMPLEMENT F) = (meet F) ` )
assume F <> {} ; ::_thesis: union (COMPLEMENT F) = (meet F) `
then union (COMPLEMENT F) = ([#] T) \ (meet F) by SETFAM_1:34
.= T \ (meet F) ;
hence union (COMPLEMENT F) = (meet F) ` ; ::_thesis: verum
end;
Lm1: for T being 1-sorted
for F being Subset-Family of T st COMPLEMENT F is finite holds
F is finite
proof
let T be 1-sorted ; ::_thesis: for F being Subset-Family of T st COMPLEMENT F is finite holds
F is finite
let F be Subset-Family of T; ::_thesis: ( COMPLEMENT F is finite implies F is finite )
defpred S1[ set , set ] means for X being Subset of T st X = $1 holds
$2 = X ` ;
A1: for x being set st x in COMPLEMENT F holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in COMPLEMENT F implies ex y being set st S1[x,y] )
assume x in COMPLEMENT F ; ::_thesis: ex y being set st S1[x,y]
then reconsider X = x as Subset of T ;
reconsider y = X ` as set ;
take y ; ::_thesis: S1[x,y]
thus S1[x,y] ; ::_thesis: verum
end;
consider f being Function such that
A2: dom f = COMPLEMENT F and
A3: for x being set st x in COMPLEMENT F holds
S1[x,f . x] from CLASSES1:sch_1(A1);
for x being set holds
( x in rng f iff x in F )
proof
let x be set ; ::_thesis: ( x in rng f iff x in F )
hereby ::_thesis: ( x in F implies x in rng f )
assume x in rng f ; ::_thesis: x in F
then consider y being set such that
A4: y in dom f and
A5: x = f . y by FUNCT_1:def_3;
reconsider Y = y as Subset of T by A2, A4;
Y ` in F by A2, A4, SETFAM_1:def_7;
hence x in F by A2, A3, A4, A5; ::_thesis: verum
end;
assume A6: x in F ; ::_thesis: x in rng f
then reconsider X = x as Subset of T ;
A7: (X `) ` = X ;
then X ` in COMPLEMENT F by A6, SETFAM_1:def_7;
then A8: f . (X `) = (X `) ` by A3;
X ` in dom f by A2, A6, A7, SETFAM_1:def_7;
hence x in rng f by A8, FUNCT_1:def_3; ::_thesis: verum
end;
then rng f = F by TARSKI:1;
then A9: f .: (COMPLEMENT F) = F by A2, RELAT_1:113;
assume COMPLEMENT F is finite ; ::_thesis: F is finite
hence F is finite by A9, FINSET_1:5; ::_thesis: verum
end;
theorem Th8: :: TOPS_2:8
for T being 1-sorted
for F being Subset-Family of T holds
( COMPLEMENT F is finite iff F is finite )
proof
let T be 1-sorted ; ::_thesis: for F being Subset-Family of T holds
( COMPLEMENT F is finite iff F is finite )
let F be Subset-Family of T; ::_thesis: ( COMPLEMENT F is finite iff F is finite )
thus ( COMPLEMENT F is finite implies F is finite ) by Lm1; ::_thesis: ( F is finite implies COMPLEMENT F is finite )
assume F is finite ; ::_thesis: COMPLEMENT F is finite
then COMPLEMENT (COMPLEMENT F) is finite ;
hence COMPLEMENT F is finite by Lm1; ::_thesis: verum
end;
definition
let T be TopStruct ;
let F be Subset-Family of T;
attrF is open means :Def1: :: TOPS_2:def 1
for P being Subset of T st P in F holds
P is open ;
attrF is closed means :Def2: :: TOPS_2:def 2
for P being Subset of T st P in F holds
P is closed ;
end;
:: deftheorem Def1 defines open TOPS_2:def_1_:_
for T being TopStruct
for F being Subset-Family of T holds
( F is open iff for P being Subset of T st P in F holds
P is open );
:: deftheorem Def2 defines closed TOPS_2:def_2_:_
for T being TopStruct
for F being Subset-Family of T holds
( F is closed iff for P being Subset of T st P in F holds
P is closed );
theorem Th9: :: TOPS_2:9
for T being TopStruct
for F being Subset-Family of T holds
( F is closed iff COMPLEMENT F is open )
proof
let T be TopStruct ; ::_thesis: for F being Subset-Family of T holds
( F is closed iff COMPLEMENT F is open )
let F be Subset-Family of T; ::_thesis: ( F is closed iff COMPLEMENT F is open )
thus ( F is closed implies COMPLEMENT F is open ) ::_thesis: ( COMPLEMENT F is open implies F is closed )
proof
assume A1: F is closed ; ::_thesis: COMPLEMENT F is open
let P be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( P in COMPLEMENT F implies P is open )
assume P in COMPLEMENT F ; ::_thesis: P is open
then P ` in F by SETFAM_1:def_7;
then P ` is closed by A1, Def2;
hence P is open by TOPS_1:4; ::_thesis: verum
end;
assume A2: COMPLEMENT F is open ; ::_thesis: F is closed
let P be Subset of T; :: according to TOPS_2:def_2 ::_thesis: ( P in F implies P is closed )
assume A3: P in F ; ::_thesis: P is closed
(P `) ` = P ;
then P ` in COMPLEMENT F by A3, SETFAM_1:def_7;
then P ` is open by A2, Def1;
hence P is closed by TOPS_1:3; ::_thesis: verum
end;
theorem :: TOPS_2:10
for T being TopStruct
for F being Subset-Family of T holds
( F is open iff COMPLEMENT F is closed )
proof
let T be TopStruct ; ::_thesis: for F being Subset-Family of T holds
( F is open iff COMPLEMENT F is closed )
let F be Subset-Family of T; ::_thesis: ( F is open iff COMPLEMENT F is closed )
F = COMPLEMENT (COMPLEMENT F) ;
hence ( F is open iff COMPLEMENT F is closed ) by Th9; ::_thesis: verum
end;
theorem :: TOPS_2:11
for T being TopStruct
for F, G being Subset-Family of T st F c= G & G is open holds
F is open
proof
let T be TopStruct ; ::_thesis: for F, G being Subset-Family of T st F c= G & G is open holds
F is open
let F, G be Subset-Family of T; ::_thesis: ( F c= G & G is open implies F is open )
assume A1: ( F c= G & G is open ) ; ::_thesis: F is open
let P be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( P in F implies P is open )
assume P in F ; ::_thesis: P is open
hence P is open by A1, Def1; ::_thesis: verum
end;
theorem :: TOPS_2:12
for T being TopStruct
for F, G being Subset-Family of T st F c= G & G is closed holds
F is closed
proof
let T be TopStruct ; ::_thesis: for F, G being Subset-Family of T st F c= G & G is closed holds
F is closed
let F, G be Subset-Family of T; ::_thesis: ( F c= G & G is closed implies F is closed )
assume A1: ( F c= G & G is closed ) ; ::_thesis: F is closed
let P be Subset of T; :: according to TOPS_2:def_2 ::_thesis: ( P in F implies P is closed )
assume P in F ; ::_thesis: P is closed
hence P is closed by A1, Def2; ::_thesis: verum
end;
theorem :: TOPS_2:13
for T being TopStruct
for F, G being Subset-Family of T st F is open & G is open holds
F \/ G is open
proof
let T be TopStruct ; ::_thesis: for F, G being Subset-Family of T st F is open & G is open holds
F \/ G is open
let F, G be Subset-Family of T; ::_thesis: ( F is open & G is open implies F \/ G is open )
assume A1: ( F is open & G is open ) ; ::_thesis: F \/ G is open
let P be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( P in F \/ G implies P is open )
assume P in F \/ G ; ::_thesis: P is open
then ( P in F or P in G ) by XBOOLE_0:def_3;
hence P is open by A1, Def1; ::_thesis: verum
end;
theorem :: TOPS_2:14
for T being TopStruct
for F, G being Subset-Family of T st F is open holds
F /\ G is open
proof
let T be TopStruct ; ::_thesis: for F, G being Subset-Family of T st F is open holds
F /\ G is open
let F, G be Subset-Family of T; ::_thesis: ( F is open implies F /\ G is open )
assume A1: F is open ; ::_thesis: F /\ G is open
let P be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( P in F /\ G implies P is open )
assume P in F /\ G ; ::_thesis: P is open
then P in F by XBOOLE_0:def_4;
hence P is open by A1, Def1; ::_thesis: verum
end;
theorem :: TOPS_2:15
for T being TopStruct
for F, G being Subset-Family of T st F is open holds
F \ G is open
proof
let T be TopStruct ; ::_thesis: for F, G being Subset-Family of T st F is open holds
F \ G is open
let F, G be Subset-Family of T; ::_thesis: ( F is open implies F \ G is open )
assume A1: F is open ; ::_thesis: F \ G is open
let P be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( P in F \ G implies P is open )
assume P in F \ G ; ::_thesis: P is open
then P in F by XBOOLE_0:def_5;
hence P is open by A1, Def1; ::_thesis: verum
end;
theorem :: TOPS_2:16
for T being TopStruct
for F, G being Subset-Family of T st F is closed & G is closed holds
F \/ G is closed
proof
let T be TopStruct ; ::_thesis: for F, G being Subset-Family of T st F is closed & G is closed holds
F \/ G is closed
let F, G be Subset-Family of T; ::_thesis: ( F is closed & G is closed implies F \/ G is closed )
assume A1: ( F is closed & G is closed ) ; ::_thesis: F \/ G is closed
let P be Subset of T; :: according to TOPS_2:def_2 ::_thesis: ( P in F \/ G implies P is closed )
assume P in F \/ G ; ::_thesis: P is closed
then ( P in F or P in G ) by XBOOLE_0:def_3;
hence P is closed by A1, Def2; ::_thesis: verum
end;
theorem :: TOPS_2:17
for T being TopStruct
for F, G being Subset-Family of T st F is closed holds
F /\ G is closed
proof
let T be TopStruct ; ::_thesis: for F, G being Subset-Family of T st F is closed holds
F /\ G is closed
let F, G be Subset-Family of T; ::_thesis: ( F is closed implies F /\ G is closed )
assume A1: F is closed ; ::_thesis: F /\ G is closed
let P be Subset of T; :: according to TOPS_2:def_2 ::_thesis: ( P in F /\ G implies P is closed )
assume P in F /\ G ; ::_thesis: P is closed
then P in F by XBOOLE_0:def_4;
hence P is closed by A1, Def2; ::_thesis: verum
end;
theorem :: TOPS_2:18
for T being TopStruct
for F, G being Subset-Family of T st F is closed holds
F \ G is closed
proof
let T be TopStruct ; ::_thesis: for F, G being Subset-Family of T st F is closed holds
F \ G is closed
let F, G be Subset-Family of T; ::_thesis: ( F is closed implies F \ G is closed )
assume A1: F is closed ; ::_thesis: F \ G is closed
let P be Subset of T; :: according to TOPS_2:def_2 ::_thesis: ( P in F \ G implies P is closed )
assume P in F \ G ; ::_thesis: P is closed
then P in F by XBOOLE_0:def_5;
hence P is closed by A1, Def2; ::_thesis: verum
end;
theorem Th19: :: TOPS_2:19
for GX being TopSpace
for W being Subset-Family of GX st W is open holds
union W is open
proof
let GX be TopSpace; ::_thesis: for W being Subset-Family of GX st W is open holds
union W is open
let W be Subset-Family of GX; ::_thesis: ( W is open implies union W is open )
assume A1: W is open ; ::_thesis: union W is open
W c= the topology of GX
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in W or x in the topology of GX )
assume A2: x in W ; ::_thesis: x in the topology of GX
then reconsider X = x as Subset of GX ;
X is open by A1, A2, Def1;
hence x in the topology of GX by PRE_TOPC:def_2; ::_thesis: verum
end;
then union W in the topology of GX by PRE_TOPC:def_1;
hence union W is open by PRE_TOPC:def_2; ::_thesis: verum
end;
theorem Th20: :: TOPS_2:20
for GX being TopSpace
for W being Subset-Family of GX st W is open & W is finite holds
meet W is open
proof
let GX be TopSpace; ::_thesis: for W being Subset-Family of GX st W is open & W is finite holds
meet W is open
let W be Subset-Family of GX; ::_thesis: ( W is open & W is finite implies meet W is open )
assume that
A1: W is open and
A2: W is finite ; ::_thesis: meet W is open
consider p being FinSequence such that
A3: rng p = W by A2, FINSEQ_1:52;
consider n being Nat such that
A4: dom p = Seg n by FINSEQ_1:def_2;
defpred S1[ Nat] means for Z being Subset-Family of GX st Z = p .: (Seg $1) & $1 <= n & 1 <= n holds
meet Z is open ;
A5: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A6: for Z being Subset-Family of GX st Z = p .: (Seg k) & k <= n & 1 <= n holds
meet Z is open ; ::_thesis: S1[k + 1]
let Z be Subset-Family of GX; ::_thesis: ( Z = p .: (Seg (k + 1)) & k + 1 <= n & 1 <= n implies meet Z is open )
assume A7: Z = p .: (Seg (k + 1)) ; ::_thesis: ( not k + 1 <= n or not 1 <= n or meet Z is open )
assume that
A8: k + 1 <= n and
A9: 1 <= n ; ::_thesis: meet Z is open
A10: now__::_thesis:_(_0_<_k_implies_meet_Z_is_open_)
reconsider G2 = Im (p,(k + 1)) as Subset-Family of GX by A3, Th2, RELAT_1:111;
reconsider G1 = p .: (Seg k) as Subset-Family of GX by A3, Th2, RELAT_1:111;
assume A11: 0 < k ; ::_thesis: meet Z is open
k + 1 <= n + 1 by A8, NAT_1:12;
then k <= n by XREAL_1:6;
then Seg k c= dom p by A4, FINSEQ_1:5;
then A12: G1 <> {} by A11, RELAT_1:119;
k + 1 <= n + 1 by A8, NAT_1:12;
then k <= n by XREAL_1:6;
then A13: meet G1 is open by A6, A9;
( 0 <= k & 0 + 1 = 1 ) by NAT_1:2;
then 1 <= k + 1 by XREAL_1:7;
then A14: k + 1 in dom p by A4, A8, FINSEQ_1:1;
then G2 = {(p . (k + 1))} by FUNCT_1:59;
then A15: meet G2 = p . (k + 1) by SETFAM_1:10;
{(k + 1)} c= dom p by A14, ZFMISC_1:31;
then A16: G2 <> {} by RELAT_1:119;
p . (k + 1) in W by A3, A14, FUNCT_1:def_3;
then A17: meet G2 is open by A1, A15, Def1;
p .: (Seg (k + 1)) = p .: ((Seg k) \/ {(k + 1)}) by FINSEQ_1:9
.= (p .: (Seg k)) \/ (p .: {(k + 1)}) by RELAT_1:120 ;
then meet Z = (meet G1) /\ (meet G2) by A7, A12, A16, SETFAM_1:9;
hence meet Z is open by A13, A17, TOPS_1:11; ::_thesis: verum
end;
now__::_thesis:_(_k_=_0_implies_meet_Z_is_open_)
assume A18: k = 0 ; ::_thesis: meet Z is open
then A19: 1 in dom p by A4, A8, FINSEQ_1:1;
then Im (p,1) = {(p . 1)} by FUNCT_1:59;
then meet Z = p . 1 by A7, A18, FINSEQ_1:2, SETFAM_1:10;
then meet Z in W by A3, A19, FUNCT_1:def_3;
hence meet Z is open by A1, Def1; ::_thesis: verum
end;
hence meet Z is open by A10, NAT_1:3; ::_thesis: verum
end;
A20: S1[ 0 ]
proof
let Z be Subset-Family of GX; ::_thesis: ( Z = p .: (Seg 0) & 0 <= n & 1 <= n implies meet Z is open )
assume that
A21: Z = p .: (Seg 0) and
0 <= n ; ::_thesis: ( not 1 <= n or meet Z is open )
A22: {} in the topology of GX by PRE_TOPC:1;
meet Z = {} by A21, SETFAM_1:1;
hence ( not 1 <= n or meet Z is open ) by A22, PRE_TOPC:def_2; ::_thesis: verum
end;
A23: for k being Nat holds S1[k] from NAT_1:sch_2(A20, A5);
A24: now__::_thesis:_(_1_<=_n_implies_meet_W_is_open_)
assume A25: 1 <= n ; ::_thesis: meet W is open
W = p .: (Seg n) by A3, A4, RELAT_1:113;
hence meet W is open by A23, A25; ::_thesis: verum
end;
A26: now__::_thesis:_(_n_=_0_implies_meet_W_is_open_)
assume n = 0 ; ::_thesis: meet W is open
then Seg n = {} ;
then W = p .: {} by A3, A4, RELAT_1:113;
then A27: meet W = {} by SETFAM_1:1;
{} in the topology of GX by PRE_TOPC:1;
hence meet W is open by A27, PRE_TOPC:def_2; ::_thesis: verum
end;
now__::_thesis:_(_n_<>_0_implies_1_<=_n_)
assume n <> 0 ; ::_thesis: 1 <= n
then A28: 0 < n by NAT_1:3;
1 = 0 + 1 ;
hence 1 <= n by A28, NAT_1:13; ::_thesis: verum
end;
hence meet W is open by A24, A26; ::_thesis: verum
end;
theorem :: TOPS_2:21
for GX being TopSpace
for W being Subset-Family of GX st W is closed & W is finite holds
union W is closed
proof
let GX be TopSpace; ::_thesis: for W being Subset-Family of GX st W is closed & W is finite holds
union W is closed
let W be Subset-Family of GX; ::_thesis: ( W is closed & W is finite implies union W is closed )
reconsider C = COMPLEMENT W as Subset-Family of GX ;
assume ( W is closed & W is finite ) ; ::_thesis: union W is closed
then ( COMPLEMENT W is open & COMPLEMENT W is finite ) by Th8, Th9;
then A1: meet C is open by Th20;
now__::_thesis:_(_W_<>_{}_implies_union_W_is_closed_)
assume W <> {} ; ::_thesis: union W is closed
then meet (COMPLEMENT W) = (union W) ` by Th6;
hence union W is closed by A1, TOPS_1:3; ::_thesis: verum
end;
hence union W is closed by ZFMISC_1:2; ::_thesis: verum
end;
theorem :: TOPS_2:22
for GX being TopSpace
for W being Subset-Family of GX st W is closed holds
meet W is closed
proof
let GX be TopSpace; ::_thesis: for W being Subset-Family of GX st W is closed holds
meet W is closed
let W be Subset-Family of GX; ::_thesis: ( W is closed implies meet W is closed )
reconsider C = COMPLEMENT W as Subset-Family of GX ;
assume W is closed ; ::_thesis: meet W is closed
then COMPLEMENT W is open by Th9;
then A1: union C is open by Th19;
A2: now__::_thesis:_(_W_<>_{}_implies_meet_W_is_closed_)
assume W <> {} ; ::_thesis: meet W is closed
then union (COMPLEMENT W) = (meet W) ` by Th7;
hence meet W is closed by A1, TOPS_1:3; ::_thesis: verum
end;
now__::_thesis:_(_W_=_{}_implies_meet_W_is_closed_)
assume W = {} ; ::_thesis: meet W is closed
then meet W = {} GX by SETFAM_1:def_1;
hence meet W is closed ; ::_thesis: verum
end;
hence meet W is closed by A2; ::_thesis: verum
end;
theorem :: TOPS_2:23
for T being TopStruct
for A being SubSpace of T
for F being Subset-Family of A holds F is Subset-Family of T
proof
let T be TopStruct ; ::_thesis: for A being SubSpace of T
for F being Subset-Family of A holds F is Subset-Family of T
let A be SubSpace of T; ::_thesis: for F being Subset-Family of A holds F is Subset-Family of T
let F be Subset-Family of A; ::_thesis: F is Subset-Family of T
[#] A c= [#] T by PRE_TOPC:def_4;
then bool the carrier of A c= bool the carrier of T by ZFMISC_1:67;
hence F is Subset-Family of T by XBOOLE_1:1; ::_thesis: verum
end;
theorem Th24: :: TOPS_2:24
for T being TopStruct
for A being SubSpace of T
for B being Subset of A holds
( B is open iff ex C being Subset of T st
( C is open & C /\ ([#] A) = B ) )
proof
let T be TopStruct ; ::_thesis: for A being SubSpace of T
for B being Subset of A holds
( B is open iff ex C being Subset of T st
( C is open & C /\ ([#] A) = B ) )
let A be SubSpace of T; ::_thesis: for B being Subset of A holds
( B is open iff ex C being Subset of T st
( C is open & C /\ ([#] A) = B ) )
let B be Subset of A; ::_thesis: ( B is open iff ex C being Subset of T st
( C is open & C /\ ([#] A) = B ) )
hereby ::_thesis: ( ex C being Subset of T st
( C is open & C /\ ([#] A) = B ) implies B is open )
assume B is open ; ::_thesis: ex C being Subset of T st
( C is open & C /\ ([#] A) = B )
then B in the topology of A by PRE_TOPC:def_2;
then consider C being Subset of T such that
A1: ( C in the topology of T & C /\ ([#] A) = B ) by PRE_TOPC:def_4;
reconsider C = C as Subset of T ;
take C = C; ::_thesis: ( C is open & C /\ ([#] A) = B )
thus ( C is open & C /\ ([#] A) = B ) by A1, PRE_TOPC:def_2; ::_thesis: verum
end;
given C being Subset of T such that A2: C is open and
A3: C /\ ([#] A) = B ; ::_thesis: B is open
C in the topology of T by A2, PRE_TOPC:def_2;
then B in the topology of A by A3, PRE_TOPC:def_4;
hence B is open by PRE_TOPC:def_2; ::_thesis: verum
end;
theorem Th25: :: TOPS_2:25
for T being TopStruct
for Q being Subset of T
for A being SubSpace of T st Q is open holds
for P being Subset of A st P = Q holds
P is open
proof
let T be TopStruct ; ::_thesis: for Q being Subset of T
for A being SubSpace of T st Q is open holds
for P being Subset of A st P = Q holds
P is open
let Q be Subset of T; ::_thesis: for A being SubSpace of T st Q is open holds
for P being Subset of A st P = Q holds
P is open
let A be SubSpace of T; ::_thesis: ( Q is open implies for P being Subset of A st P = Q holds
P is open )
assume A1: Q is open ; ::_thesis: for P being Subset of A st P = Q holds
P is open
let P be Subset of A; ::_thesis: ( P = Q implies P is open )
assume P = Q ; ::_thesis: P is open
then Q /\ ([#] A) = P by XBOOLE_1:28;
hence P is open by A1, Th24; ::_thesis: verum
end;
theorem Th26: :: TOPS_2:26
for T being TopStruct
for Q being Subset of T
for A being SubSpace of T st Q is closed holds
for P being Subset of A st P = Q holds
P is closed
proof
let T be TopStruct ; ::_thesis: for Q being Subset of T
for A being SubSpace of T st Q is closed holds
for P being Subset of A st P = Q holds
P is closed
let Q be Subset of T; ::_thesis: for A being SubSpace of T st Q is closed holds
for P being Subset of A st P = Q holds
P is closed
let A be SubSpace of T; ::_thesis: ( Q is closed implies for P being Subset of A st P = Q holds
P is closed )
assume A1: Q is closed ; ::_thesis: for P being Subset of A st P = Q holds
P is closed
let P be Subset of A; ::_thesis: ( P = Q implies P is closed )
assume P = Q ; ::_thesis: P is closed
then Q /\ ([#] A) = P by XBOOLE_1:28;
hence P is closed by A1, PRE_TOPC:13; ::_thesis: verum
end;
theorem :: TOPS_2:27
for T being TopStruct
for F being Subset-Family of T
for A being SubSpace of T st F is open holds
for G being Subset-Family of A st G = F holds
G is open
proof
let T be TopStruct ; ::_thesis: for F being Subset-Family of T
for A being SubSpace of T st F is open holds
for G being Subset-Family of A st G = F holds
G is open
let F be Subset-Family of T; ::_thesis: for A being SubSpace of T st F is open holds
for G being Subset-Family of A st G = F holds
G is open
let A be SubSpace of T; ::_thesis: ( F is open implies for G being Subset-Family of A st G = F holds
G is open )
assume A1: F is open ; ::_thesis: for G being Subset-Family of A st G = F holds
G is open
let G be Subset-Family of A; ::_thesis: ( G = F implies G is open )
assume A2: G = F ; ::_thesis: G is open
let P be Subset of A; :: according to TOPS_2:def_1 ::_thesis: ( P in G implies P is open )
assume A3: P in G ; ::_thesis: P is open
reconsider PP = P as Subset of T by PRE_TOPC:11;
PP is open by A1, A2, A3, Def1;
hence P is open by Th25; ::_thesis: verum
end;
theorem :: TOPS_2:28
for T being TopStruct
for F being Subset-Family of T
for A being SubSpace of T st F is closed holds
for G being Subset-Family of A st G = F holds
G is closed
proof
let T be TopStruct ; ::_thesis: for F being Subset-Family of T
for A being SubSpace of T st F is closed holds
for G being Subset-Family of A st G = F holds
G is closed
let F be Subset-Family of T; ::_thesis: for A being SubSpace of T st F is closed holds
for G being Subset-Family of A st G = F holds
G is closed
let A be SubSpace of T; ::_thesis: ( F is closed implies for G being Subset-Family of A st G = F holds
G is closed )
assume A1: F is closed ; ::_thesis: for G being Subset-Family of A st G = F holds
G is closed
let G be Subset-Family of A; ::_thesis: ( G = F implies G is closed )
assume A2: G = F ; ::_thesis: G is closed
let P be Subset of A; :: according to TOPS_2:def_2 ::_thesis: ( P in G implies P is closed )
assume A3: P in G ; ::_thesis: P is closed
reconsider PP = P as Subset of T by PRE_TOPC:11;
PP is closed by A1, A2, A3, Def2;
hence P is closed by Th26; ::_thesis: verum
end;
theorem Th29: :: TOPS_2:29
for T being TopStruct
for M, N being Subset of T holds M /\ N is Subset of (T | N)
proof
let T be TopStruct ; ::_thesis: for M, N being Subset of T holds M /\ N is Subset of (T | N)
let M, N be Subset of T; ::_thesis: M /\ N is Subset of (T | N)
M /\ N c= N by XBOOLE_1:17;
then M /\ N c= [#] (T | N) by PRE_TOPC:def_5;
hence M /\ N is Subset of (T | N) ; ::_thesis: verum
end;
definition
let T be TopStruct ;
let P be Subset of T;
let F be Subset-Family of T;
funcF | P -> Subset-Family of (T | P) means :Def3: :: TOPS_2:def 3
for Q being Subset of (T | P) holds
( Q in it iff ex R being Subset of T st
( R in F & R /\ P = Q ) );
existence
ex b1 being Subset-Family of (T | P) st
for Q being Subset of (T | P) holds
( Q in b1 iff ex R being Subset of T st
( R in F & R /\ P = Q ) )
proof
thus ex G being Subset-Family of (T | P) st
for Q being Subset of (T | P) holds
( Q in G iff ex R being Subset of T st
( R in F & R /\ P = Q ) ) ::_thesis: verum
proof
defpred S1[ Subset of (T | P)] means ex R being Subset of T st
( R in F & R /\ P = $1 );
ex G being Subset-Family of (T | P) st
for Q being Subset of (T | P) holds
( Q in G iff S1[Q] ) from SUBSET_1:sch_3();
hence ex G being Subset-Family of (T | P) st
for Q being Subset of (T | P) holds
( Q in G iff ex R being Subset of T st
( R in F & R /\ P = Q ) ) ; ::_thesis: verum
end;
end;
uniqueness
for b1, b2 being Subset-Family of (T | P) st ( for Q being Subset of (T | P) holds
( Q in b1 iff ex R being Subset of T st
( R in F & R /\ P = Q ) ) ) & ( for Q being Subset of (T | P) holds
( Q in b2 iff ex R being Subset of T st
( R in F & R /\ P = Q ) ) ) holds
b1 = b2
proof
thus for G, H being Subset-Family of (T | P) st ( for Q being Subset of (T | P) holds
( Q in G iff ex R being Subset of T st
( R in F & R /\ P = Q ) ) ) & ( for Q being Subset of (T | P) holds
( Q in H iff ex R being Subset of T st
( R in F & R /\ P = Q ) ) ) holds
G = H ::_thesis: verum
proof
let G, H be Subset-Family of (T | P); ::_thesis: ( ( for Q being Subset of (T | P) holds
( Q in G iff ex R being Subset of T st
( R in F & R /\ P = Q ) ) ) & ( for Q being Subset of (T | P) holds
( Q in H iff ex R being Subset of T st
( R in F & R /\ P = Q ) ) ) implies G = H )
assume that
A1: for Q being Subset of (T | P) holds
( Q in G iff ex R being Subset of T st
( R in F & R /\ P = Q ) ) and
A2: for Q being Subset of (T | P) holds
( Q in H iff ex R being Subset of T st
( R in F & R /\ P = Q ) ) ; ::_thesis: G = H
for x being set holds
( x in G iff x in H )
proof
let x be set ; ::_thesis: ( x in G iff x in H )
hereby ::_thesis: ( x in H implies x in G )
assume A3: x in G ; ::_thesis: x in H
then reconsider X = x as Subset of (T | P) ;
ex R being Subset of T st
( R in F & R /\ P = X ) by A1, A3;
hence x in H by A2; ::_thesis: verum
end;
assume A4: x in H ; ::_thesis: x in G
then reconsider X = x as Subset of (T | P) ;
ex R being Subset of T st
( R in F & R /\ P = X ) by A2, A4;
hence x in G by A1; ::_thesis: verum
end;
hence G = H by TARSKI:1; ::_thesis: verum
end;
end;
end;
:: deftheorem Def3 defines | TOPS_2:def_3_:_
for T being TopStruct
for P being Subset of T
for F being Subset-Family of T
for b4 being Subset-Family of (T | P) holds
( b4 = F | P iff for Q being Subset of (T | P) holds
( Q in b4 iff ex R being Subset of T st
( R in F & R /\ P = Q ) ) );
theorem :: TOPS_2:30
for T being TopStruct
for M being Subset of T
for F, G being Subset-Family of T st F c= G holds
F | M c= G | M
proof
let T be TopStruct ; ::_thesis: for M being Subset of T
for F, G being Subset-Family of T st F c= G holds
F | M c= G | M
let M be Subset of T; ::_thesis: for F, G being Subset-Family of T st F c= G holds
F | M c= G | M
let F, G be Subset-Family of T; ::_thesis: ( F c= G implies F | M c= G | M )
assume A1: F c= G ; ::_thesis: F | M c= G | M
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F | M or x in G | M )
assume A2: x in F | M ; ::_thesis: x in G | M
then reconsider X = x as Subset of (T | M) ;
ex R being Subset of T st
( R in F & R /\ M = X ) by A2, Def3;
hence x in G | M by A1, Def3; ::_thesis: verum
end;
theorem Th31: :: TOPS_2:31
for T being TopStruct
for Q, M being Subset of T
for F being Subset-Family of T st Q in F holds
Q /\ M in F | M
proof
let T be TopStruct ; ::_thesis: for Q, M being Subset of T
for F being Subset-Family of T st Q in F holds
Q /\ M in F | M
let Q, M be Subset of T; ::_thesis: for F being Subset-Family of T st Q in F holds
Q /\ M in F | M
let F be Subset-Family of T; ::_thesis: ( Q in F implies Q /\ M in F | M )
reconsider QQ = Q /\ M as Subset of (T | M) by Th29;
A1: Q /\ M = QQ ;
assume Q in F ; ::_thesis: Q /\ M in F | M
hence Q /\ M in F | M by A1, Def3; ::_thesis: verum
end;
theorem :: TOPS_2:32
for T being TopStruct
for Q, M being Subset of T
for F being Subset-Family of T st Q c= union F holds
Q /\ M c= union (F | M)
proof
let T be TopStruct ; ::_thesis: for Q, M being Subset of T
for F being Subset-Family of T st Q c= union F holds
Q /\ M c= union (F | M)
let Q, M be Subset of T; ::_thesis: for F being Subset-Family of T st Q c= union F holds
Q /\ M c= union (F | M)
let F be Subset-Family of T; ::_thesis: ( Q c= union F implies Q /\ M c= union (F | M) )
assume A1: Q c= union F ; ::_thesis: Q /\ M c= union (F | M)
now__::_thesis:_(_M_<>_{}_implies_Q_/\_M_c=_union_(F_|_M)_)
assume M <> {} ; ::_thesis: Q /\ M c= union (F | M)
thus Q /\ M c= union (F | M) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Q /\ M or x in union (F | M) )
assume A2: x in Q /\ M ; ::_thesis: x in union (F | M)
then x in Q by XBOOLE_0:def_4;
then consider Z being set such that
A3: x in Z and
A4: Z in F by A1, TARSKI:def_4;
reconsider ZZ = Z as Subset of T by A4;
ZZ /\ M in F | M by A4, Th31;
then reconsider ZP = ZZ /\ M as Subset of (T | M) ;
A5: ZP in F | M by A4, Th31;
x in M by A2, XBOOLE_0:def_4;
then x in ZP by A3, XBOOLE_0:def_4;
hence x in union (F | M) by A5, TARSKI:def_4; ::_thesis: verum
end;
end;
hence Q /\ M c= union (F | M) by XBOOLE_1:2; ::_thesis: verum
end;
theorem :: TOPS_2:33
for T being TopStruct
for M being Subset of T
for F being Subset-Family of T st M c= union F holds
M = union (F | M)
proof
let T be TopStruct ; ::_thesis: for M being Subset of T
for F being Subset-Family of T st M c= union F holds
M = union (F | M)
let M be Subset of T; ::_thesis: for F being Subset-Family of T st M c= union F holds
M = union (F | M)
let F be Subset-Family of T; ::_thesis: ( M c= union F implies M = union (F | M) )
assume A1: M c= union F ; ::_thesis: M = union (F | M)
for x being set holds
( x in M iff x in union (F | M) )
proof
let x be set ; ::_thesis: ( x in M iff x in union (F | M) )
hereby ::_thesis: ( x in union (F | M) implies x in M )
assume A2: x in M ; ::_thesis: x in union (F | M)
then consider A being set such that
A3: x in A and
A4: A in F by A1, TARSKI:def_4;
reconsider A9 = A as Subset of T by A4;
A /\ M c= M by XBOOLE_1:17;
then A /\ M c= [#] (T | M) by PRE_TOPC:def_5;
then reconsider B = A9 /\ M as Subset of (T | M) ;
A5: B in F | M by A4, Def3;
x in A /\ M by A2, A3, XBOOLE_0:def_4;
hence x in union (F | M) by A5, TARSKI:def_4; ::_thesis: verum
end;
assume x in union (F | M) ; ::_thesis: x in M
then consider A being set such that
A6: x in A and
A7: A in F | M by TARSKI:def_4;
reconsider B = A as Subset of (T | M) by A7;
ex R being Subset of T st
( R in F & R /\ M = B ) by A7, Def3;
hence x in M by A6, XBOOLE_0:def_4; ::_thesis: verum
end;
hence M = union (F | M) by TARSKI:1; ::_thesis: verum
end;
theorem Th34: :: TOPS_2:34
for T being TopStruct
for M being Subset of T
for F being Subset-Family of T holds union (F | M) c= union F
proof
let T be TopStruct ; ::_thesis: for M being Subset of T
for F being Subset-Family of T holds union (F | M) c= union F
let M be Subset of T; ::_thesis: for F being Subset-Family of T holds union (F | M) c= union F
let F be Subset-Family of T; ::_thesis: union (F | M) c= union F
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (F | M) or x in union F )
assume x in union (F | M) ; ::_thesis: x in union F
then consider A being set such that
A1: x in A and
A2: A in F | M by TARSKI:def_4;
reconsider Q = A as Subset of (T | M) by A2;
consider R being Subset of T such that
A3: R in F and
A4: R /\ M = Q by A2, Def3;
x in R by A1, A4, XBOOLE_0:def_4;
hence x in union F by A3, TARSKI:def_4; ::_thesis: verum
end;
theorem :: TOPS_2:35
for T being TopStruct
for M being Subset of T
for F being Subset-Family of T st M c= union (F | M) holds
M c= union F
proof
let T be TopStruct ; ::_thesis: for M being Subset of T
for F being Subset-Family of T st M c= union (F | M) holds
M c= union F
let M be Subset of T; ::_thesis: for F being Subset-Family of T st M c= union (F | M) holds
M c= union F
let F be Subset-Family of T; ::_thesis: ( M c= union (F | M) implies M c= union F )
assume A1: M c= union (F | M) ; ::_thesis: M c= union F
union (F | M) c= union F by Th34;
hence M c= union F by A1, XBOOLE_1:1; ::_thesis: verum
end;
theorem :: TOPS_2:36
for T being TopStruct
for M being Subset of T
for F being Subset-Family of T st F is finite holds
F | M is finite
proof
let T be TopStruct ; ::_thesis: for M being Subset of T
for F being Subset-Family of T st F is finite holds
F | M is finite
let M be Subset of T; ::_thesis: for F being Subset-Family of T st F is finite holds
F | M is finite
let F be Subset-Family of T; ::_thesis: ( F is finite implies F | M is finite )
defpred S1[ set , set ] means for X being Subset of T st X = $1 holds
$2 = X /\ M;
A1: for x being set st x in F holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in F implies ex y being set st S1[x,y] )
assume x in F ; ::_thesis: ex y being set st S1[x,y]
then reconsider X = x as Subset of T ;
reconsider y = X /\ M as set ;
take y ; ::_thesis: S1[x,y]
thus S1[x,y] ; ::_thesis: verum
end;
consider f being Function such that
A2: dom f = F and
A3: for x being set st x in F holds
S1[x,f . x] from CLASSES1:sch_1(A1);
for x being set holds
( x in rng f iff x in F | M )
proof
let x be set ; ::_thesis: ( x in rng f iff x in F | M )
hereby ::_thesis: ( x in F | M implies x in rng f )
assume x in rng f ; ::_thesis: x in F | M
then consider y being set such that
A4: y in dom f and
A5: x = f . y by FUNCT_1:def_3;
reconsider Y = y as Subset of T by A2, A4;
Y /\ M c= M by XBOOLE_1:17;
then Y /\ M c= [#] (T | M) by PRE_TOPC:def_5;
then reconsider X = f . y as Subset of (T | M) by A2, A3, A4;
f . y = Y /\ M by A2, A3, A4;
then X in F | M by A2, A4, Def3;
hence x in F | M by A5; ::_thesis: verum
end;
assume A6: x in F | M ; ::_thesis: x in rng f
then reconsider X = x as Subset of (T | M) ;
consider R being Subset of T such that
A7: R in F and
A8: R /\ M = X by A6, Def3;
f . R = R /\ M by A3, A7;
hence x in rng f by A2, A7, A8, FUNCT_1:def_3; ::_thesis: verum
end;
then rng f = F | M by TARSKI:1;
then A9: f .: F = F | M by A2, RELAT_1:113;
assume F is finite ; ::_thesis: F | M is finite
hence F | M is finite by A9, FINSET_1:5; ::_thesis: verum
end;
theorem :: TOPS_2:37
for T being TopStruct
for M being Subset of T
for F being Subset-Family of T st F is open holds
F | M is open
proof
let T be TopStruct ; ::_thesis: for M being Subset of T
for F being Subset-Family of T st F is open holds
F | M is open
let M be Subset of T; ::_thesis: for F being Subset-Family of T st F is open holds
F | M is open
let F be Subset-Family of T; ::_thesis: ( F is open implies F | M is open )
assume A1: F is open ; ::_thesis: F | M is open
let Q be Subset of (T | M); :: according to TOPS_2:def_1 ::_thesis: ( Q in F | M implies Q is open )
assume Q in F | M ; ::_thesis: Q is open
then consider R being Subset of T such that
A2: R in F and
A3: R /\ M = Q by Def3;
reconsider R = R as Subset of T ;
A4: Q = R /\ ([#] (T | M)) by A3, PRE_TOPC:def_5;
R is open by A1, A2, Def1;
hence Q is open by A4, Th24; ::_thesis: verum
end;
theorem :: TOPS_2:38
for T being TopStruct
for M being Subset of T
for F being Subset-Family of T st F is closed holds
F | M is closed
proof
let T be TopStruct ; ::_thesis: for M being Subset of T
for F being Subset-Family of T st F is closed holds
F | M is closed
let M be Subset of T; ::_thesis: for F being Subset-Family of T st F is closed holds
F | M is closed
let F be Subset-Family of T; ::_thesis: ( F is closed implies F | M is closed )
assume A1: F is closed ; ::_thesis: F | M is closed
let Q be Subset of (T | M); :: according to TOPS_2:def_2 ::_thesis: ( Q in F | M implies Q is closed )
assume Q in F | M ; ::_thesis: Q is closed
then consider R being Subset of T such that
A2: R in F and
A3: R /\ M = Q by Def3;
reconsider R = R as Subset of T ;
A4: Q = R /\ ([#] (T | M)) by A3, PRE_TOPC:def_5;
R is closed by A1, A2, Def2;
hence Q is closed by A4, PRE_TOPC:13; ::_thesis: verum
end;
theorem :: TOPS_2:39
for T being TopStruct
for A being SubSpace of T
for F being Subset-Family of A st F is open holds
ex G being Subset-Family of T st
( G is open & ( for AA being Subset of T st AA = [#] A holds
F = G | AA ) )
proof
let T be TopStruct ; ::_thesis: for A being SubSpace of T
for F being Subset-Family of A st F is open holds
ex G being Subset-Family of T st
( G is open & ( for AA being Subset of T st AA = [#] A holds
F = G | AA ) )
let A be SubSpace of T; ::_thesis: for F being Subset-Family of A st F is open holds
ex G being Subset-Family of T st
( G is open & ( for AA being Subset of T st AA = [#] A holds
F = G | AA ) )
let F be Subset-Family of A; ::_thesis: ( F is open implies ex G being Subset-Family of T st
( G is open & ( for AA being Subset of T st AA = [#] A holds
F = G | AA ) ) )
assume A1: F is open ; ::_thesis: ex G being Subset-Family of T st
( G is open & ( for AA being Subset of T st AA = [#] A holds
F = G | AA ) )
[#] A c= [#] T by PRE_TOPC:def_4;
then reconsider At = [#] A as Subset of T ;
defpred S1[ Subset of T] means ex X1 being Subset of T st
( X1 = $1 & X1 is open & $1 /\ At in F );
consider G being Subset-Family of T such that
A2: for X being Subset of T holds
( X in G iff S1[X] ) from SUBSET_1:sch_3();
take G ; ::_thesis: ( G is open & ( for AA being Subset of T st AA = [#] A holds
F = G | AA ) )
thus G is open ::_thesis: for AA being Subset of T st AA = [#] A holds
F = G | AA
proof
let H be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( H in G implies H is open )
assume H in G ; ::_thesis: H is open
then ex X1 being Subset of T st
( X1 = H & X1 is open & H /\ At in F ) by A2;
hence H is open ; ::_thesis: verum
end;
let AA be Subset of T; ::_thesis: ( AA = [#] A implies F = G | AA )
assume A3: AA = [#] A ; ::_thesis: F = G | AA
then F c= bool AA ;
then F c= bool ([#] (T | AA)) by PRE_TOPC:def_5;
then reconsider FF = F as Subset-Family of (T | AA) ;
for X being Subset of (T | AA) holds
( X in FF iff ex X9 being Subset of T st
( X9 in G & X9 /\ AA = X ) )
proof
let X be Subset of (T | AA); ::_thesis: ( X in FF iff ex X9 being Subset of T st
( X9 in G & X9 /\ AA = X ) )
thus ( X in FF implies ex X9 being Subset of T st
( X9 in G & X9 /\ AA = X ) ) ::_thesis: ( ex X9 being Subset of T st
( X9 in G & X9 /\ AA = X ) implies X in FF )
proof
assume A4: X in FF ; ::_thesis: ex X9 being Subset of T st
( X9 in G & X9 /\ AA = X )
then reconsider XX = X as Subset of A ;
XX is open by A1, A4, Def1;
then consider Y being Subset of T such that
A5: ( Y is open & Y /\ ([#] A) = XX ) by Th24;
take Y ; ::_thesis: ( Y in G & Y /\ AA = X )
thus ( Y in G & Y /\ AA = X ) by A2, A3, A4, A5; ::_thesis: verum
end;
given X9 being Subset of T such that A6: X9 in G and
A7: X9 /\ AA = X ; ::_thesis: X in FF
ex X1 being Subset of T st
( X1 = X9 & X1 is open & X9 /\ At in F ) by A2, A6;
hence X in FF by A3, A7; ::_thesis: verum
end;
hence F = G | AA by Def3; ::_thesis: verum
end;
theorem :: TOPS_2:40
for T being TopStruct
for P being Subset of T
for F being Subset-Family of T ex f being Function st
( dom f = F & rng f = F | P & ( for x being set st x in F holds
for Q being Subset of T st Q = x holds
f . x = Q /\ P ) )
proof
let T be TopStruct ; ::_thesis: for P being Subset of T
for F being Subset-Family of T ex f being Function st
( dom f = F & rng f = F | P & ( for x being set st x in F holds
for Q being Subset of T st Q = x holds
f . x = Q /\ P ) )
let P be Subset of T; ::_thesis: for F being Subset-Family of T ex f being Function st
( dom f = F & rng f = F | P & ( for x being set st x in F holds
for Q being Subset of T st Q = x holds
f . x = Q /\ P ) )
let F be Subset-Family of T; ::_thesis: ex f being Function st
( dom f = F & rng f = F | P & ( for x being set st x in F holds
for Q being Subset of T st Q = x holds
f . x = Q /\ P ) )
defpred S1[ set , set ] means for Q being Subset of T st Q = $1 holds
$2 = Q /\ P;
A1: for x being set st x in F holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in F implies ex y being set st S1[x,y] )
assume x in F ; ::_thesis: ex y being set st S1[x,y]
then reconsider Q = x as Subset of T ;
reconsider y = Q /\ P as set ;
take y ; ::_thesis: S1[x,y]
thus S1[x,y] ; ::_thesis: verum
end;
consider f being Function such that
A2: dom f = F and
A3: for x being set st x in F holds
S1[x,f . x] from CLASSES1:sch_1(A1);
take f ; ::_thesis: ( dom f = F & rng f = F | P & ( for x being set st x in F holds
for Q being Subset of T st Q = x holds
f . x = Q /\ P ) )
thus dom f = F by A2; ::_thesis: ( rng f = F | P & ( for x being set st x in F holds
for Q being Subset of T st Q = x holds
f . x = Q /\ P ) )
for x being set holds
( x in rng f iff x in F | P )
proof
let x be set ; ::_thesis: ( x in rng f iff x in F | P )
hereby ::_thesis: ( x in F | P implies x in rng f )
assume x in rng f ; ::_thesis: x in F | P
then consider y being set such that
A4: y in dom f and
A5: f . y = x by FUNCT_1:def_3;
reconsider Y = y as Subset of T by A2, A4;
Y /\ P c= P by XBOOLE_1:17;
then Y /\ P c= [#] (T | P) by PRE_TOPC:def_5;
then reconsider X = x as Subset of (T | P) by A2, A3, A4, A5;
X = Y /\ P by A2, A3, A4, A5;
hence x in F | P by A2, A4, Def3; ::_thesis: verum
end;
assume A6: x in F | P ; ::_thesis: x in rng f
then reconsider X = x as Subset of (T | P) ;
consider Q being Subset of T such that
A7: Q in F and
A8: Q /\ P = X by A6, Def3;
reconsider p = Q as set ;
f . p = x by A3, A7, A8;
hence x in rng f by A2, A7, FUNCT_1:def_3; ::_thesis: verum
end;
hence rng f = F | P by TARSKI:1; ::_thesis: for x being set st x in F holds
for Q being Subset of T st Q = x holds
f . x = Q /\ P
thus for x being set st x in F holds
for Q being Subset of T st Q = x holds
f . x = Q /\ P by A3; ::_thesis: verum
end;
theorem Th41: :: TOPS_2:41
for X, Y being 1-sorted
for f being Function of X,Y st ( [#] Y = {} implies [#] X = {} ) holds
f " ([#] Y) = [#] X
proof
let X, Y be 1-sorted ; ::_thesis: for f being Function of X,Y st ( [#] Y = {} implies [#] X = {} ) holds
f " ([#] Y) = [#] X
let f be Function of X,Y; ::_thesis: ( ( [#] Y = {} implies [#] X = {} ) implies f " ([#] Y) = [#] X )
assume A1: ( [#] Y = {} implies [#] X = {} ) ; ::_thesis: f " ([#] Y) = [#] X
f " (rng f) = dom f by RELAT_1:134
.= [#] X by A1, FUNCT_2:def_1 ;
then [#] X c= f " ([#] Y) by RELAT_1:143;
hence f " ([#] Y) = [#] X by XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: TOPS_2:42
for T being 1-sorted
for S being non empty 1-sorted
for f being Function of T,S
for H being Subset-Family of S holds (" f) .: H is Subset-Family of T
proof
let T be 1-sorted ; ::_thesis: for S being non empty 1-sorted
for f being Function of T,S
for H being Subset-Family of S holds (" f) .: H is Subset-Family of T
let S be non empty 1-sorted ; ::_thesis: for f being Function of T,S
for H being Subset-Family of S holds (" f) .: H is Subset-Family of T
let f be Function of T,S; ::_thesis: for H being Subset-Family of S holds (" f) .: H is Subset-Family of T
let H be Subset-Family of S; ::_thesis: (" f) .: H is Subset-Family of T
( (" f) .: H c= rng (" f) & rng (" f) c= bool (dom f) ) by FUNCT_3:22, RELAT_1:111;
then (" f) .: H c= bool (dom f) by XBOOLE_1:1;
hence (" f) .: H is Subset-Family of T by FUNCT_2:def_1; ::_thesis: verum
end;
theorem Th43: :: TOPS_2:43
for X, Y being TopStruct
for f being Function of X,Y st ( [#] Y = {} implies [#] X = {} ) holds
( f is continuous iff for P being Subset of Y st P is open holds
f " P is open )
proof
let X, Y be TopStruct ; ::_thesis: for f being Function of X,Y st ( [#] Y = {} implies [#] X = {} ) holds
( f is continuous iff for P being Subset of Y st P is open holds
f " P is open )
let f be Function of X,Y; ::_thesis: ( ( [#] Y = {} implies [#] X = {} ) implies ( f is continuous iff for P being Subset of Y st P is open holds
f " P is open ) )
assume A1: ( [#] Y = {} implies [#] X = {} ) ; ::_thesis: ( f is continuous iff for P being Subset of Y st P is open holds
f " P is open )
hereby ::_thesis: ( ( for P being Subset of Y st P is open holds
f " P is open ) implies f is continuous )
assume A2: f is continuous ; ::_thesis: for P1 being Subset of Y st P1 is open holds
f " P1 is open
let P1 be Subset of Y; ::_thesis: ( P1 is open implies f " P1 is open )
assume P1 is open ; ::_thesis: f " P1 is open
then P1 ` is closed by TOPS_1:4;
then A3: f " (P1 `) is closed by A2, PRE_TOPC:def_6;
f " (P1 `) = (f " ([#] Y)) \ (f " P1) by FUNCT_1:69
.= ([#] X) \ (f " P1) by A1, Th41
.= (f " P1) ` ;
hence f " P1 is open by A3, TOPS_1:4; ::_thesis: verum
end;
assume A4: for P1 being Subset of Y st P1 is open holds
f " P1 is open ; ::_thesis: f is continuous
let P1 be Subset of Y; :: according to PRE_TOPC:def_6 ::_thesis: ( not P1 is closed or f " P1 is closed )
assume P1 is closed ; ::_thesis: f " P1 is closed
then P1 ` is open by TOPS_1:3;
then A5: f " (P1 `) is open by A4;
f " (P1 `) = (f " ([#] Y)) \ (f " P1) by FUNCT_1:69
.= ([#] X) \ (f " P1) by A1, Th41
.= (f " P1) ` ;
hence f " P1 is closed by A5, TOPS_1:3; ::_thesis: verum
end;
theorem Th44: :: TOPS_2:44
for T, S being TopSpace
for f being Function of T,S holds
( f is continuous iff for P1 being Subset of S holds Cl (f " P1) c= f " (Cl P1) )
proof
let T, S be TopSpace; ::_thesis: for f being Function of T,S holds
( f is continuous iff for P1 being Subset of S holds Cl (f " P1) c= f " (Cl P1) )
let f be Function of T,S; ::_thesis: ( f is continuous iff for P1 being Subset of S holds Cl (f " P1) c= f " (Cl P1) )
hereby ::_thesis: ( ( for P1 being Subset of S holds Cl (f " P1) c= f " (Cl P1) ) implies f is continuous )
assume A1: f is continuous ; ::_thesis: for P1 being Subset of S holds Cl (f " P1) c= f " (Cl P1)
let P1 be Subset of S; ::_thesis: Cl (f " P1) c= f " (Cl P1)
Cl (Cl P1) = Cl P1 ;
then Cl P1 is closed by PRE_TOPC:22;
then A2: f " (Cl P1) is closed by A1, PRE_TOPC:def_6;
f " P1 c= f " (Cl P1) by PRE_TOPC:18, RELAT_1:143;
then Cl (f " P1) c= Cl (f " (Cl P1)) by PRE_TOPC:19;
hence Cl (f " P1) c= f " (Cl P1) by A2, PRE_TOPC:22; ::_thesis: verum
end;
assume A3: for P1 being Subset of S holds Cl (f " P1) c= f " (Cl P1) ; ::_thesis: f is continuous
let P1 be Subset of S; :: according to PRE_TOPC:def_6 ::_thesis: ( not P1 is closed or f " P1 is closed )
assume P1 is closed ; ::_thesis: f " P1 is closed
then Cl P1 = P1 by PRE_TOPC:22;
then ( f " P1 c= Cl (f " P1) & Cl (f " P1) c= f " P1 ) by A3, PRE_TOPC:18;
then f " P1 = Cl (f " P1) by XBOOLE_0:def_10;
hence f " P1 is closed by PRE_TOPC:22; ::_thesis: verum
end;
theorem Th45: :: TOPS_2:45
for T being TopSpace
for S being non empty TopSpace
for f being Function of T,S holds
( f is continuous iff for P being Subset of T holds f .: (Cl P) c= Cl (f .: P) )
proof
let T be TopSpace; ::_thesis: for S being non empty TopSpace
for f being Function of T,S holds
( f is continuous iff for P being Subset of T holds f .: (Cl P) c= Cl (f .: P) )
let S be non empty TopSpace; ::_thesis: for f being Function of T,S holds
( f is continuous iff for P being Subset of T holds f .: (Cl P) c= Cl (f .: P) )
let f be Function of T,S; ::_thesis: ( f is continuous iff for P being Subset of T holds f .: (Cl P) c= Cl (f .: P) )
hereby ::_thesis: ( ( for P being Subset of T holds f .: (Cl P) c= Cl (f .: P) ) implies f is continuous )
assume A1: f is continuous ; ::_thesis: for P being Subset of T holds f .: (Cl P) c= Cl (f .: P)
let P be Subset of T; ::_thesis: f .: (Cl P) c= Cl (f .: P)
P c= [#] T ;
then P c= dom f by FUNCT_2:def_1;
then A2: Cl P c= Cl (f " (f .: P)) by FUNCT_1:76, PRE_TOPC:19;
Cl (f " (f .: P)) c= f " (Cl (f .: P)) by A1, Th44;
then Cl P c= f " (Cl (f .: P)) by A2, XBOOLE_1:1;
then A3: f .: (Cl P) c= f .: (f " (Cl (f .: P))) by RELAT_1:123;
f .: (f " (Cl (f .: P))) c= Cl (f .: P) by FUNCT_1:75;
hence f .: (Cl P) c= Cl (f .: P) by A3, XBOOLE_1:1; ::_thesis: verum
end;
assume A4: for P being Subset of T holds f .: (Cl P) c= Cl (f .: P) ; ::_thesis: f is continuous
now__::_thesis:_for_P1_being_Subset_of_S_holds_Cl_(f_"_P1)_c=_f_"_(Cl_P1)
let P1 be Subset of S; ::_thesis: Cl (f " P1) c= f " (Cl P1)
Cl (f " P1) c= [#] T ;
then Cl (f " P1) c= dom f by FUNCT_2:def_1;
then A5: Cl (f " P1) c= f " (f .: (Cl (f " P1))) by FUNCT_1:76;
( f .: (Cl (f " P1)) c= Cl (f .: (f " P1)) & Cl (f .: (f " P1)) c= Cl P1 ) by A4, FUNCT_1:75, PRE_TOPC:19;
then f .: (Cl (f " P1)) c= Cl P1 by XBOOLE_1:1;
then f " (f .: (Cl (f " P1))) c= f " (Cl P1) by RELAT_1:143;
hence Cl (f " P1) c= f " (Cl P1) by A5, XBOOLE_1:1; ::_thesis: verum
end;
hence f is continuous by Th44; ::_thesis: verum
end;
theorem Th46: :: TOPS_2:46
for T, V being TopStruct
for S being non empty TopStruct
for f being Function of T,S
for g being Function of S,V st f is continuous & g is continuous holds
g * f is continuous
proof
let T, V be TopStruct ; ::_thesis: for S being non empty TopStruct
for f being Function of T,S
for g being Function of S,V st f is continuous & g is continuous holds
g * f is continuous
let S be non empty TopStruct ; ::_thesis: for f being Function of T,S
for g being Function of S,V st f is continuous & g is continuous holds
g * f is continuous
let f be Function of T,S; ::_thesis: for g being Function of S,V st f is continuous & g is continuous holds
g * f is continuous
let g be Function of S,V; ::_thesis: ( f is continuous & g is continuous implies g * f is continuous )
assume that
A1: f is continuous and
A2: g is continuous ; ::_thesis: g * f is continuous
let P be Subset of V; :: according to PRE_TOPC:def_6 ::_thesis: ( not P is closed or (g * f) " P is closed )
assume P is closed ; ::_thesis: (g * f) " P is closed
then ( (g * f) " P = f " (g " P) & g " P is closed ) by A2, PRE_TOPC:def_6, RELAT_1:146;
hence (g * f) " P is closed by A1, PRE_TOPC:def_6; ::_thesis: verum
end;
theorem :: TOPS_2:47
for T being TopStruct
for S being non empty TopStruct
for f being Function of T,S
for H being Subset-Family of S st f is continuous & H is open holds
for F being Subset-Family of T st F = (" f) .: H holds
F is open
proof
let T be TopStruct ; ::_thesis: for S being non empty TopStruct
for f being Function of T,S
for H being Subset-Family of S st f is continuous & H is open holds
for F being Subset-Family of T st F = (" f) .: H holds
F is open
let S be non empty TopStruct ; ::_thesis: for f being Function of T,S
for H being Subset-Family of S st f is continuous & H is open holds
for F being Subset-Family of T st F = (" f) .: H holds
F is open
let f be Function of T,S; ::_thesis: for H being Subset-Family of S st f is continuous & H is open holds
for F being Subset-Family of T st F = (" f) .: H holds
F is open
let H be Subset-Family of S; ::_thesis: ( f is continuous & H is open implies for F being Subset-Family of T st F = (" f) .: H holds
F is open )
assume that
A1: f is continuous and
A2: H is open ; ::_thesis: for F being Subset-Family of T st F = (" f) .: H holds
F is open
let F be Subset-Family of T; ::_thesis: ( F = (" f) .: H implies F is open )
assume A3: F = (" f) .: H ; ::_thesis: F is open
let X be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( X in F implies X is open )
assume X in F ; ::_thesis: X is open
then consider y being set such that
A4: y in dom (" f) and
A5: y in H and
A6: X = (" f) . y by A3, FUNCT_1:def_6;
reconsider Y = y as Subset of S by A5;
A7: X = f " Y by A4, A6, FUNCT_3:21;
A8: ( [#] S = {} implies [#] T = {} ) ;
Y is open by A2, A5, Def1;
hence X is open by A1, A8, A7, Th43; ::_thesis: verum
end;
theorem :: TOPS_2:48
for T, S being TopStruct
for f being Function of T,S
for H being Subset-Family of S st f is continuous & H is closed holds
for F being Subset-Family of T st F = (" f) .: H holds
F is closed
proof
let T, S be TopStruct ; ::_thesis: for f being Function of T,S
for H being Subset-Family of S st f is continuous & H is closed holds
for F being Subset-Family of T st F = (" f) .: H holds
F is closed
let f be Function of T,S; ::_thesis: for H being Subset-Family of S st f is continuous & H is closed holds
for F being Subset-Family of T st F = (" f) .: H holds
F is closed
let H be Subset-Family of S; ::_thesis: ( f is continuous & H is closed implies for F being Subset-Family of T st F = (" f) .: H holds
F is closed )
assume that
A1: f is continuous and
A2: H is closed ; ::_thesis: for F being Subset-Family of T st F = (" f) .: H holds
F is closed
let F be Subset-Family of T; ::_thesis: ( F = (" f) .: H implies F is closed )
assume A3: F = (" f) .: H ; ::_thesis: F is closed
let X be Subset of T; :: according to TOPS_2:def_2 ::_thesis: ( X in F implies X is closed )
assume X in F ; ::_thesis: X is closed
then consider y being set such that
A4: y in dom (" f) and
A5: y in H and
A6: X = (" f) . y by A3, FUNCT_1:def_6;
reconsider Y = y as Subset of S by A5;
A7: X = f " Y by A4, A6, FUNCT_3:21;
Y is closed by A2, A5, Def2;
hence X is closed by A1, A7, PRE_TOPC:def_6; ::_thesis: verum
end;
definition
let S, T be set ;
let f be Function of S,T;
assume A1: f is bijective ;
funcf /" -> Function of T,S equals :Def4: :: TOPS_2:def 4
f " ;
coherence
f " is Function of T,S
proof
rng f = [#] T by A1, FUNCT_2:def_3;
hence f " is Function of T,S by A1, FUNCT_2:25; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines /" TOPS_2:def_4_:_
for S, T being set
for f being Function of S,T st f is bijective holds
f /" = f " ;
notation
let S, T be set ;
let f be Function of S,T;
synonym f " for f /" ;
end;
theorem Th49: :: TOPS_2:49
for T being 1-sorted
for S being non empty 1-sorted
for f being Function of T,S st rng f = [#] S & f is one-to-one holds
( dom (f ") = [#] S & rng (f ") = [#] T )
proof
let T be 1-sorted ; ::_thesis: for S being non empty 1-sorted
for f being Function of T,S st rng f = [#] S & f is one-to-one holds
( dom (f ") = [#] S & rng (f ") = [#] T )
let S be non empty 1-sorted ; ::_thesis: for f being Function of T,S st rng f = [#] S & f is one-to-one holds
( dom (f ") = [#] S & rng (f ") = [#] T )
let f be Function of T,S; ::_thesis: ( rng f = [#] S & f is one-to-one implies ( dom (f ") = [#] S & rng (f ") = [#] T ) )
assume that
A1: rng f = [#] S and
A2: f is one-to-one ; ::_thesis: ( dom (f ") = [#] S & rng (f ") = [#] T )
A3: f is onto by A1, FUNCT_2:def_3;
hence dom (f ") = dom (f ") by A2, Def4
.= [#] S by A1, A2, FUNCT_1:32 ;
::_thesis: rng (f ") = [#] T
thus rng (f ") = rng (f ") by A2, A3, Def4
.= dom f by A2, FUNCT_1:33
.= [#] T by FUNCT_2:def_1 ; ::_thesis: verum
end;
theorem Th50: :: TOPS_2:50
for T, S being 1-sorted
for f being Function of T,S st rng f = [#] S & f is one-to-one holds
f " is one-to-one
proof
let T, S be 1-sorted ; ::_thesis: for f being Function of T,S st rng f = [#] S & f is one-to-one holds
f " is one-to-one
let f be Function of T,S; ::_thesis: ( rng f = [#] S & f is one-to-one implies f " is one-to-one )
assume that
A1: rng f = [#] S and
A2: f is one-to-one ; ::_thesis: f " is one-to-one
A3: f is onto by A1, FUNCT_2:def_3;
f " is one-to-one by A2;
hence f " is one-to-one by A2, A3, Def4; ::_thesis: verum
end;
theorem Th51: :: TOPS_2:51
for T being 1-sorted
for S being non empty 1-sorted
for f being Function of T,S st rng f = [#] S & f is one-to-one holds
(f ") " = f
proof
let T be 1-sorted ; ::_thesis: for S being non empty 1-sorted
for f being Function of T,S st rng f = [#] S & f is one-to-one holds
(f ") " = f
let S be non empty 1-sorted ; ::_thesis: for f being Function of T,S st rng f = [#] S & f is one-to-one holds
(f ") " = f
let f be Function of T,S; ::_thesis: ( rng f = [#] S & f is one-to-one implies (f ") " = f )
assume that
A1: rng f = [#] S and
A2: f is one-to-one ; ::_thesis: (f ") " = f
A3: f is onto by A1, FUNCT_2:def_3;
f = (f ") " by A2, FUNCT_1:43;
then A4: f = (f ") " by A3, A2, Def4;
A5: f " is one-to-one by A1, A2, Th50;
rng (f ") = [#] T by A1, A2, Th49;
then f " is onto by FUNCT_2:def_3;
hence (f ") " = f by A4, A5, Def4; ::_thesis: verum
end;
theorem :: TOPS_2:52
for T, S being 1-sorted
for f being Function of T,S st rng f = [#] S & f is one-to-one holds
( (f ") * f = id (dom f) & f * (f ") = id (rng f) )
proof
let T, S be 1-sorted ; ::_thesis: for f being Function of T,S st rng f = [#] S & f is one-to-one holds
( (f ") * f = id (dom f) & f * (f ") = id (rng f) )
let f be Function of T,S; ::_thesis: ( rng f = [#] S & f is one-to-one implies ( (f ") * f = id (dom f) & f * (f ") = id (rng f) ) )
assume that
A1: rng f = [#] S and
A2: f is one-to-one ; ::_thesis: ( (f ") * f = id (dom f) & f * (f ") = id (rng f) )
A3: f is onto by A1, FUNCT_2:def_3;
( (f ") * f = id (dom f) & f * (f ") = id (rng f) ) by A2, FUNCT_1:39;
hence ( (f ") * f = id (dom f) & f * (f ") = id (rng f) ) by A2, A3, Def4; ::_thesis: verum
end;
theorem Th53: :: TOPS_2:53
for T being 1-sorted
for S, V being non empty 1-sorted
for f being Function of T,S
for g being Function of S,V st rng f = [#] S & f is one-to-one & dom g = [#] S & rng g = [#] V & g is one-to-one holds
(g * f) " = (f ") * (g ")
proof
let T be 1-sorted ; ::_thesis: for S, V being non empty 1-sorted
for f being Function of T,S
for g being Function of S,V st rng f = [#] S & f is one-to-one & dom g = [#] S & rng g = [#] V & g is one-to-one holds
(g * f) " = (f ") * (g ")
let S, V be non empty 1-sorted ; ::_thesis: for f being Function of T,S
for g being Function of S,V st rng f = [#] S & f is one-to-one & dom g = [#] S & rng g = [#] V & g is one-to-one holds
(g * f) " = (f ") * (g ")
let f be Function of T,S; ::_thesis: for g being Function of S,V st rng f = [#] S & f is one-to-one & dom g = [#] S & rng g = [#] V & g is one-to-one holds
(g * f) " = (f ") * (g ")
let g be Function of S,V; ::_thesis: ( rng f = [#] S & f is one-to-one & dom g = [#] S & rng g = [#] V & g is one-to-one implies (g * f) " = (f ") * (g ") )
assume that
A1: rng f = [#] S and
A2: f is one-to-one ; ::_thesis: ( not dom g = [#] S or not rng g = [#] V or not g is one-to-one or (g * f) " = (f ") * (g ") )
assume that
A3: dom g = [#] S and
A4: rng g = [#] V and
A5: g is one-to-one ; ::_thesis: (g * f) " = (f ") * (g ")
A6: ( f is onto & g is onto ) by A1, A4, FUNCT_2:def_3;
rng (g * f) = [#] V by A1, A3, A4, RELAT_1:28;
then g * f is onto by FUNCT_2:def_3;
then A7: (g * f) " = (g * f) " by A2, A5, Def4;
A8: f " = f " by A2, A6, Def4;
g " = g " by A5, A6, Def4;
hence (g * f) " = (f ") * (g ") by A2, A5, A8, A7, FUNCT_1:44; ::_thesis: verum
end;
theorem Th54: :: TOPS_2:54
for T, S being 1-sorted
for f being Function of T,S
for P being Subset of T st rng f = [#] S & f is one-to-one holds
f .: P = (f ") " P
proof
let T, S be 1-sorted ; ::_thesis: for f being Function of T,S
for P being Subset of T st rng f = [#] S & f is one-to-one holds
f .: P = (f ") " P
let f be Function of T,S; ::_thesis: for P being Subset of T st rng f = [#] S & f is one-to-one holds
f .: P = (f ") " P
let P be Subset of T; ::_thesis: ( rng f = [#] S & f is one-to-one implies f .: P = (f ") " P )
assume that
A1: rng f = [#] S and
A2: f is one-to-one ; ::_thesis: f .: P = (f ") " P
A3: f is onto by A1, FUNCT_2:def_3;
f .: P = (f ") " P by A2, FUNCT_1:84;
hence f .: P = (f ") " P by A2, A3, Def4; ::_thesis: verum
end;
theorem Th55: :: TOPS_2:55
for T, S being 1-sorted
for f being Function of T,S
for P1 being Subset of S st rng f = [#] S & f is one-to-one holds
f " P1 = (f ") .: P1
proof
let T, S be 1-sorted ; ::_thesis: for f being Function of T,S
for P1 being Subset of S st rng f = [#] S & f is one-to-one holds
f " P1 = (f ") .: P1
let f be Function of T,S; ::_thesis: for P1 being Subset of S st rng f = [#] S & f is one-to-one holds
f " P1 = (f ") .: P1
let P1 be Subset of S; ::_thesis: ( rng f = [#] S & f is one-to-one implies f " P1 = (f ") .: P1 )
assume rng f = [#] S ; ::_thesis: ( not f is one-to-one or f " P1 = (f ") .: P1 )
then A1: f is onto by FUNCT_2:def_3;
assume A2: f is one-to-one ; ::_thesis: f " P1 = (f ") .: P1
f " P1 = (f ") .: P1 by A2, FUNCT_1:85;
hence f " P1 = (f ") .: P1 by A1, A2, Def4; ::_thesis: verum
end;
definition
let S, T be TopStruct ;
let f be Function of S,T;
attrf is being_homeomorphism means :Def5: :: TOPS_2:def 5
( dom f = [#] S & rng f = [#] T & f is one-to-one & f is continuous & f " is continuous );
end;
:: deftheorem Def5 defines being_homeomorphism TOPS_2:def_5_:_
for S, T being TopStruct
for f being Function of S,T holds
( f is being_homeomorphism iff ( dom f = [#] S & rng f = [#] T & f is one-to-one & f is continuous & f " is continuous ) );
theorem :: TOPS_2:56
for T being TopStruct
for S being non empty TopStruct
for f being Function of T,S st f is being_homeomorphism holds
f " is being_homeomorphism
proof
let T be TopStruct ; ::_thesis: for S being non empty TopStruct
for f being Function of T,S st f is being_homeomorphism holds
f " is being_homeomorphism
let S be non empty TopStruct ; ::_thesis: for f being Function of T,S st f is being_homeomorphism holds
f " is being_homeomorphism
let f be Function of T,S; ::_thesis: ( f is being_homeomorphism implies f " is being_homeomorphism )
assume A1: f is being_homeomorphism ; ::_thesis: f " is being_homeomorphism
then A2: ( rng f = [#] S & f is one-to-one ) by Def5;
hence ( dom (f ") = [#] S & rng (f ") = [#] T ) by Th49; :: according to TOPS_2:def_5 ::_thesis: ( f " is one-to-one & f " is continuous & (f ") " is continuous )
thus f " is one-to-one by A2, Th50; ::_thesis: ( f " is continuous & (f ") " is continuous )
thus f " is continuous by A1, Def5; ::_thesis: (f ") " is continuous
f is continuous by A1, Def5;
hence (f ") " is continuous by A2, Th51; ::_thesis: verum
end;
theorem :: TOPS_2:57
for T, S, V being non empty TopStruct
for f being Function of T,S
for g being Function of S,V st f is being_homeomorphism & g is being_homeomorphism holds
g * f is being_homeomorphism
proof
let T, S, V be non empty TopStruct ; ::_thesis: for f being Function of T,S
for g being Function of S,V st f is being_homeomorphism & g is being_homeomorphism holds
g * f is being_homeomorphism
let f be Function of T,S; ::_thesis: for g being Function of S,V st f is being_homeomorphism & g is being_homeomorphism holds
g * f is being_homeomorphism
let g be Function of S,V; ::_thesis: ( f is being_homeomorphism & g is being_homeomorphism implies g * f is being_homeomorphism )
assume that
A1: f is being_homeomorphism and
A2: g is being_homeomorphism ; ::_thesis: g * f is being_homeomorphism
A3: ( rng f = [#] S & dom g = [#] S ) by A1, A2, Def5;
A4: rng g = [#] V by A2, Def5;
dom f = [#] T by A1, Def5;
hence ( dom (g * f) = [#] T & rng (g * f) = [#] V ) by A3, A4, RELAT_1:27, RELAT_1:28; :: according to TOPS_2:def_5 ::_thesis: ( g * f is one-to-one & g * f is continuous & (g * f) " is continuous )
A5: ( f is one-to-one & g is one-to-one ) by A1, A2, Def5;
hence g * f is one-to-one ; ::_thesis: ( g * f is continuous & (g * f) " is continuous )
( f is continuous & g is continuous ) by A1, A2, Def5;
hence g * f is continuous by Th46; ::_thesis: (g * f) " is continuous
( f " is continuous & g " is continuous ) by A1, A2, Def5;
then (f ") * (g ") is continuous by Th46;
hence (g * f) " is continuous by A3, A4, A5, Th53; ::_thesis: verum
end;
theorem :: TOPS_2:58
for T being TopStruct
for S being non empty TopStruct
for f being Function of T,S holds
( f is being_homeomorphism iff ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P being Subset of T holds
( P is closed iff f .: P is closed ) ) ) )
proof
let T be TopStruct ; ::_thesis: for S being non empty TopStruct
for f being Function of T,S holds
( f is being_homeomorphism iff ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P being Subset of T holds
( P is closed iff f .: P is closed ) ) ) )
let S be non empty TopStruct ; ::_thesis: for f being Function of T,S holds
( f is being_homeomorphism iff ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P being Subset of T holds
( P is closed iff f .: P is closed ) ) ) )
let f be Function of T,S; ::_thesis: ( f is being_homeomorphism iff ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P being Subset of T holds
( P is closed iff f .: P is closed ) ) ) )
hereby ::_thesis: ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P being Subset of T holds
( P is closed iff f .: P is closed ) ) implies f is being_homeomorphism )
assume A1: f is being_homeomorphism ; ::_thesis: ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P being Subset of T holds
( ( P is closed implies f .: P is closed ) & ( f .: P is closed implies P is closed ) ) ) )
hence A2: ( dom f = [#] T & rng f = [#] S & f is one-to-one ) by Def5; ::_thesis: for P being Subset of T holds
( ( P is closed implies f .: P is closed ) & ( f .: P is closed implies P is closed ) )
let P be Subset of T; ::_thesis: ( ( P is closed implies f .: P is closed ) & ( f .: P is closed implies P is closed ) )
A3: f " is continuous by A1, Def5;
hereby ::_thesis: ( f .: P is closed implies P is closed )
assume A4: P is closed ; ::_thesis: f .: P is closed
f is onto by A2, FUNCT_2:def_3;
then (f ") " P = (f ") " P by A2, Def4
.= f .: P by A2, FUNCT_1:84 ;
hence f .: P is closed by A3, A4, PRE_TOPC:def_6; ::_thesis: verum
end;
assume A5: f .: P is closed ; ::_thesis: P is closed
f is continuous by A1, Def5;
then A6: f " (f .: P) is closed by A5, PRE_TOPC:def_6;
dom f = [#] T by FUNCT_2:def_1;
then A7: P c= f " (f .: P) by FUNCT_1:76;
f " (f .: P) c= P by A2, FUNCT_1:82;
hence P is closed by A6, A7, XBOOLE_0:def_10; ::_thesis: verum
end;
assume that
A8: dom f = [#] T and
A9: rng f = [#] S and
A10: f is one-to-one ; ::_thesis: ( ex P being Subset of T st
( ( P is closed implies f .: P is closed ) implies ( f .: P is closed & not P is closed ) ) or f is being_homeomorphism )
assume A11: for P being Subset of T holds
( P is closed iff f .: P is closed ) ; ::_thesis: f is being_homeomorphism
A12: f is continuous
proof
let B be Subset of S; :: according to PRE_TOPC:def_6 ::_thesis: ( not B is closed or f " B is closed )
assume A13: B is closed ; ::_thesis: f " B is closed
set D = f " B;
B = f .: (f " B) by A9, FUNCT_1:77;
hence f " B is closed by A11, A13; ::_thesis: verum
end;
f " is continuous
proof
let B be Subset of T; :: according to PRE_TOPC:def_6 ::_thesis: ( not B is closed or (f ") " B is closed )
assume A14: B is closed ; ::_thesis: (f ") " B is closed
f is onto by A9, FUNCT_2:def_3;
then (f ") " B = (f ") " B by A10, Def4
.= f .: B by A10, FUNCT_1:84 ;
hence (f ") " B is closed by A11, A14; ::_thesis: verum
end;
hence f is being_homeomorphism by A8, A9, A10, A12, Def5; ::_thesis: verum
end;
theorem :: TOPS_2:59
for T being non empty TopSpace
for S being TopSpace
for f being Function of T,S holds
( f is being_homeomorphism iff ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P1 being Subset of S holds f " (Cl P1) = Cl (f " P1) ) ) )
proof
let T be non empty TopSpace; ::_thesis: for S being TopSpace
for f being Function of T,S holds
( f is being_homeomorphism iff ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P1 being Subset of S holds f " (Cl P1) = Cl (f " P1) ) ) )
let S be TopSpace; ::_thesis: for f being Function of T,S holds
( f is being_homeomorphism iff ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P1 being Subset of S holds f " (Cl P1) = Cl (f " P1) ) ) )
let f be Function of T,S; ::_thesis: ( f is being_homeomorphism iff ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P1 being Subset of S holds f " (Cl P1) = Cl (f " P1) ) ) )
hereby ::_thesis: ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P1 being Subset of S holds f " (Cl P1) = Cl (f " P1) ) implies f is being_homeomorphism )
assume A1: f is being_homeomorphism ; ::_thesis: ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P1 being Subset of S holds f " (Cl P1) = Cl (f " P1) ) )
hence A2: ( dom f = [#] T & rng f = [#] S & f is one-to-one ) by Def5; ::_thesis: for P1 being Subset of S holds f " (Cl P1) = Cl (f " P1)
let P1 be Subset of S; ::_thesis: f " (Cl P1) = Cl (f " P1)
f is continuous by A1, Def5;
then A3: Cl (f " P1) c= f " (Cl P1) by Th44;
f " is continuous by A1, Def5;
then A4: (f ") .: (Cl P1) c= Cl ((f ") .: P1) by Th45;
( f " (Cl P1) = (f ") .: (Cl P1) & f " P1 = (f ") .: P1 ) by A2, Th55;
hence f " (Cl P1) = Cl (f " P1) by A3, A4, XBOOLE_0:def_10; ::_thesis: verum
end;
assume that
A5: dom f = [#] T and
A6: ( rng f = [#] S & f is one-to-one ) ; ::_thesis: ( ex P1 being Subset of S st not f " (Cl P1) = Cl (f " P1) or f is being_homeomorphism )
assume A7: for P1 being Subset of S holds f " (Cl P1) = Cl (f " P1) ; ::_thesis: f is being_homeomorphism
thus ( dom f = [#] T & rng f = [#] S & f is one-to-one ) by A5, A6; :: according to TOPS_2:def_5 ::_thesis: ( f is continuous & f " is continuous )
for P1 being Subset of S holds Cl (f " P1) c= f " (Cl P1) by A7;
hence f is continuous by Th44; ::_thesis: f " is continuous
now__::_thesis:_for_P1_being_Subset_of_S_holds_(f_")_.:_(Cl_P1)_c=_Cl_((f_")_.:_P1)
let P1 be Subset of S; ::_thesis: (f ") .: (Cl P1) c= Cl ((f ") .: P1)
( (f ") .: (Cl P1) = f " (Cl P1) & (f ") .: P1 = f " P1 ) by A6, Th55;
hence (f ") .: (Cl P1) c= Cl ((f ") .: P1) by A7; ::_thesis: verum
end;
hence f " is continuous by Th45; ::_thesis: verum
end;
theorem :: TOPS_2:60
for T being TopSpace
for S being non empty TopSpace
for f being Function of T,S holds
( f is being_homeomorphism iff ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P being Subset of T holds f .: (Cl P) = Cl (f .: P) ) ) )
proof
let T be TopSpace; ::_thesis: for S being non empty TopSpace
for f being Function of T,S holds
( f is being_homeomorphism iff ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P being Subset of T holds f .: (Cl P) = Cl (f .: P) ) ) )
let S be non empty TopSpace; ::_thesis: for f being Function of T,S holds
( f is being_homeomorphism iff ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P being Subset of T holds f .: (Cl P) = Cl (f .: P) ) ) )
let f be Function of T,S; ::_thesis: ( f is being_homeomorphism iff ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P being Subset of T holds f .: (Cl P) = Cl (f .: P) ) ) )
hereby ::_thesis: ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P being Subset of T holds f .: (Cl P) = Cl (f .: P) ) implies f is being_homeomorphism )
assume A1: f is being_homeomorphism ; ::_thesis: ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P being Subset of T holds f .: (Cl P) = Cl (f .: P) ) )
hence A2: ( dom f = [#] T & rng f = [#] S & f is one-to-one ) by Def5; ::_thesis: for P being Subset of T holds f .: (Cl P) = Cl (f .: P)
let P be Subset of T; ::_thesis: f .: (Cl P) = Cl (f .: P)
f is continuous by A1, Def5;
then A3: f .: (Cl P) c= Cl (f .: P) by Th45;
f " is continuous by A1, Def5;
then A4: Cl ((f ") " P) c= (f ") " (Cl P) by Th44;
( (f ") " P = f .: P & (f ") " (Cl P) = f .: (Cl P) ) by A2, Th54;
hence f .: (Cl P) = Cl (f .: P) by A3, A4, XBOOLE_0:def_10; ::_thesis: verum
end;
assume that
A5: dom f = [#] T and
A6: ( rng f = [#] S & f is one-to-one ) ; ::_thesis: ( ex P being Subset of T st not f .: (Cl P) = Cl (f .: P) or f is being_homeomorphism )
assume A7: for P being Subset of T holds f .: (Cl P) = Cl (f .: P) ; ::_thesis: f is being_homeomorphism
thus ( dom f = [#] T & rng f = [#] S & f is one-to-one ) by A5, A6; :: according to TOPS_2:def_5 ::_thesis: ( f is continuous & f " is continuous )
for P being Subset of T holds f .: (Cl P) c= Cl (f .: P) by A7;
hence f is continuous by Th45; ::_thesis: f " is continuous
now__::_thesis:_for_P_being_Subset_of_T_holds_Cl_((f_")_"_P)_c=_(f_")_"_(Cl_P)
let P be Subset of T; ::_thesis: Cl ((f ") " P) c= (f ") " (Cl P)
( (f ") " P = f .: P & (f ") " (Cl P) = f .: (Cl P) ) by A6, Th54;
hence Cl ((f ") " P) c= (f ") " (Cl P) by A7; ::_thesis: verum
end;
hence f " is continuous by Th44; ::_thesis: verum
end;
theorem Th61: :: TOPS_2:61
for X, Y being non empty TopSpace
for f being Function of X,Y
for A being Subset of X st f is continuous & A is connected holds
f .: A is connected
proof
let X, Y be non empty TopSpace; ::_thesis: for f being Function of X,Y
for A being Subset of X st f is continuous & A is connected holds
f .: A is connected
let f be Function of X,Y; ::_thesis: for A being Subset of X st f is continuous & A is connected holds
f .: A is connected
let A be Subset of X; ::_thesis: ( f is continuous & A is connected implies f .: A is connected )
assume A1: f is continuous ; ::_thesis: ( not A is connected or f .: A is connected )
assume A2: A is connected ; ::_thesis: f .: A is connected
assume not f .: A is connected ; ::_thesis: contradiction
then consider P, Q being Subset of Y such that
A3: f .: A = P \/ Q and
A4: P,Q are_separated and
A5: P <> {} Y and
A6: Q <> {} Y by CONNSP_1:15;
reconsider P1 = f " P, Q1 = f " Q as Subset of X ;
set P2 = P1 /\ A;
set Q2 = Q1 /\ A;
set y = the Element of P;
the Element of P in f .: A by A3, A5, XBOOLE_0:def_3;
then consider x being set such that
A7: x in dom f and
A8: x in A and
A9: the Element of P = f . x by FUNCT_1:def_6;
x in f " P by A5, A7, A9, FUNCT_1:def_7;
then A10: P1 /\ A <> {} by A8, XBOOLE_0:def_4;
A11: the carrier of X = dom f by FUNCT_2:def_1;
P misses Cl Q by A4, CONNSP_1:def_1;
then A12: ( (f " P) /\ (f " (Cl Q)) = f " (P /\ (Cl Q)) & f " (P /\ (Cl Q)) = f " ({} Y) ) by FUNCT_1:68, XBOOLE_0:def_7;
Cl Q1 c= f " (Cl Q) by A1, Th44;
then P1 /\ (Cl Q1) = {} by A12, XBOOLE_1:3, XBOOLE_1:26;
then A13: P1 misses Cl Q1 by XBOOLE_0:def_7;
Cl P misses Q by A4, CONNSP_1:def_1;
then A14: ( (f " (Cl P)) /\ (f " Q) = f " ((Cl P) /\ Q) & f " ((Cl P) /\ Q) = f " ({} Y) ) by FUNCT_1:68, XBOOLE_0:def_7;
Cl P1 c= f " (Cl P) by A1, Th44;
then (Cl P1) /\ Q1 = {} X by A14, XBOOLE_1:3, XBOOLE_1:26;
then Cl P1 misses Q1 by XBOOLE_0:def_7;
then A15: P1,Q1 are_separated by A13, CONNSP_1:def_1;
set z = the Element of Q;
the Element of Q in P \/ Q by A6, XBOOLE_0:def_3;
then consider x1 being set such that
A16: x1 in dom f and
A17: x1 in A and
A18: the Element of Q = f . x1 by A3, FUNCT_1:def_6;
x1 in f " Q by A6, A16, A18, FUNCT_1:def_7;
then A19: Q1 /\ A <> {} by A17, XBOOLE_0:def_4;
f " (f .: A) = (f " P) \/ (f " Q) by A3, RELAT_1:140;
then A20: A = (P1 \/ Q1) /\ A by A11, FUNCT_1:76, XBOOLE_1:28
.= (P1 /\ A) \/ (Q1 /\ A) by XBOOLE_1:23 ;
( P1 /\ A c= P1 & Q1 /\ A c= Q1 ) by XBOOLE_1:17;
then ex P3, Q3 being Subset of X st
( A = P3 \/ Q3 & P3,Q3 are_separated & P3 <> {} X & Q3 <> {} X ) by A15, A20, A10, A19, CONNSP_1:7;
hence contradiction by A2, CONNSP_1:15; ::_thesis: verum
end;
theorem :: TOPS_2:62
for S, T being non empty TopSpace
for f being Function of S,T
for A being Subset of T st f is being_homeomorphism & A is connected holds
f " A is connected
proof
let S, T be non empty TopSpace; ::_thesis: for f being Function of S,T
for A being Subset of T st f is being_homeomorphism & A is connected holds
f " A is connected
let f be Function of S,T; ::_thesis: for A being Subset of T st f is being_homeomorphism & A is connected holds
f " A is connected
let A be Subset of T; ::_thesis: ( f is being_homeomorphism & A is connected implies f " A is connected )
assume that
A1: f is being_homeomorphism and
A2: A is connected ; ::_thesis: f " A is connected
f " is continuous by A1, Def5;
then A3: (f ") .: A is connected by A2, Th61;
( rng f = [#] T & f is one-to-one ) by A1, Def5;
hence f " A is connected by A3, Th55; ::_thesis: verum
end;
begin
theorem :: TOPS_2:63
for GX being non empty TopSpace st ( for x, y being Point of GX ex GY being non empty TopSpace st
( GY is connected & ex f being Function of GY,GX st
( f is continuous & x in rng f & y in rng f ) ) ) holds
GX is connected
proof
let GX be non empty TopSpace; ::_thesis: ( ( for x, y being Point of GX ex GY being non empty TopSpace st
( GY is connected & ex f being Function of GY,GX st
( f is continuous & x in rng f & y in rng f ) ) ) implies GX is connected )
assume A1: for x, y being Point of GX ex GY being non empty TopSpace st
( GY is connected & ex f being Function of GY,GX st
( f is continuous & x in rng f & y in rng f ) ) ; ::_thesis: GX is connected
for A, B being Subset of GX st [#] GX = A \/ B & A <> {} GX & B <> {} GX & A is open & B is open holds
A meets B
proof
let A, B be Subset of GX; ::_thesis: ( [#] GX = A \/ B & A <> {} GX & B <> {} GX & A is open & B is open implies A meets B )
assume that
A2: [#] GX = A \/ B and
A3: A <> {} GX and
A4: B <> {} GX and
A5: ( A is open & B is open ) ; ::_thesis: A meets B
set v = the Element of B;
set u = the Element of A;
reconsider y = the Element of B as Point of GX by A2, A4, XBOOLE_0:def_3;
reconsider x = the Element of A as Point of GX by A2, A3, XBOOLE_0:def_3;
consider GY being non empty TopSpace such that
A6: GY is connected and
A7: ex f being Function of GY,GX st
( f is continuous & x in rng f & y in rng f ) by A1;
consider f being Function of GY,GX such that
A8: f is continuous and
A9: x in rng f and
A10: y in rng f by A7;
f " ([#] GX) = [#] GY by Th41;
then A11: (f " A) \/ (f " B) = [#] GY by A2, RELAT_1:140;
(rng f) /\ B <> {} by A4, A10, XBOOLE_0:def_4;
then rng f meets B by XBOOLE_0:def_7;
then A12: f " B <> {} GY by RELAT_1:138;
(rng f) /\ A <> {} by A3, A9, XBOOLE_0:def_4;
then rng f meets A by XBOOLE_0:def_7;
then A13: f " A <> {} GY by RELAT_1:138;
[#] GX <> {} ;
then ( f " A is open & f " B is open ) by A5, A8, Th43;
then f " A meets f " B by A6, A11, A13, A12, CONNSP_1:11;
then (f " A) /\ (f " B) <> {} by XBOOLE_0:def_7;
then f " (A /\ B) <> {} by FUNCT_1:68;
then rng f meets A /\ B by RELAT_1:138;
then ex u1 being set st
( u1 in rng f & u1 in A /\ B ) by XBOOLE_0:3;
hence A meets B by XBOOLE_0:4; ::_thesis: verum
end;
hence GX is connected by CONNSP_1:11; ::_thesis: verum
end;
theorem Th64: :: TOPS_2:64
for X being TopStruct
for F being Subset-Family of X holds
( F is open iff F c= the topology of X )
proof
let X be TopStruct ; ::_thesis: for F being Subset-Family of X holds
( F is open iff F c= the topology of X )
let F be Subset-Family of X; ::_thesis: ( F is open iff F c= the topology of X )
thus ( F is open implies F c= the topology of X ) ::_thesis: ( F c= the topology of X implies F is open )
proof
assume A1: F is open ; ::_thesis: F c= the topology of X
let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in F or A in the topology of X )
assume A2: A in F ; ::_thesis: A in the topology of X
then reconsider A = A as Subset of X ;
A is open by A1, A2, Def1;
hence A in the topology of X by PRE_TOPC:def_2; ::_thesis: verum
end;
assume A3: F c= the topology of X ; ::_thesis: F is open
let A be Subset of X; :: according to TOPS_2:def_1 ::_thesis: ( A in F implies A is open )
thus ( A in F implies A is open ) by A3, PRE_TOPC:def_2; ::_thesis: verum
end;
theorem :: TOPS_2:65
for X being TopStruct
for F being Subset-Family of X holds
( F is closed iff F c= COMPLEMENT the topology of X )
proof
let X be TopStruct ; ::_thesis: for F being Subset-Family of X holds
( F is closed iff F c= COMPLEMENT the topology of X )
let F be Subset-Family of X; ::_thesis: ( F is closed iff F c= COMPLEMENT the topology of X )
thus ( F is closed implies F c= COMPLEMENT the topology of X ) ::_thesis: ( F c= COMPLEMENT the topology of X implies F is closed )
proof
assume A1: F is closed ; ::_thesis: F c= COMPLEMENT the topology of X
let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in F or A in COMPLEMENT the topology of X )
assume A2: A in F ; ::_thesis: A in COMPLEMENT the topology of X
then reconsider A = A as Subset of X ;
A is closed by A1, A2, Def2;
then A ` is open by TOPS_1:3;
then A ` in the topology of X by PRE_TOPC:def_2;
hence A in COMPLEMENT the topology of X by SETFAM_1:def_7; ::_thesis: verum
end;
assume A3: F c= COMPLEMENT the topology of X ; ::_thesis: F is closed
let A be Subset of X; :: according to TOPS_2:def_2 ::_thesis: ( A in F implies A is closed )
assume A in F ; ::_thesis: A is closed
then A ` in the topology of X by A3, SETFAM_1:def_7;
then A ` is open by PRE_TOPC:def_2;
hence A is closed by TOPS_1:3; ::_thesis: verum
end;
registration
let X be TopStruct ;
cluster the topology of X -> open ;
coherence
the topology of X is open by Th64;
cluster open for Element of bool (bool the carrier of X);
existence
ex b1 being Subset-Family of X st b1 is open
proof
take the topology of X ; ::_thesis: the topology of X is open
thus the topology of X is open ; ::_thesis: verum
end;
end;