:: FIN_TOPO semantic presentation
begin
theorem Th1: :: FIN_TOPO:1
for A being set
for f being FinSequence of bool A st ( for i being Element of NAT st 1 <= i & i < len f holds
f /. i c= f /. (i + 1) ) holds
for i, j being Element of NAT st i <= j & 1 <= i & j <= len f holds
f /. i c= f /. j
proof
let A be set ; ::_thesis: for f being FinSequence of bool A st ( for i being Element of NAT st 1 <= i & i < len f holds
f /. i c= f /. (i + 1) ) holds
for i, j being Element of NAT st i <= j & 1 <= i & j <= len f holds
f /. i c= f /. j
let f be FinSequence of bool A; ::_thesis: ( ( for i being Element of NAT st 1 <= i & i < len f holds
f /. i c= f /. (i + 1) ) implies for i, j being Element of NAT st i <= j & 1 <= i & j <= len f holds
f /. i c= f /. j )
assume A1: for i being Element of NAT st 1 <= i & i < len f holds
f /. i c= f /. (i + 1) ; ::_thesis: for i, j being Element of NAT st i <= j & 1 <= i & j <= len f holds
f /. i c= f /. j
let i, j be Element of NAT ; ::_thesis: ( i <= j & 1 <= i & j <= len f implies f /. i c= f /. j )
assume that
A2: i <= j and
A3: 1 <= i and
A4: j <= len f ; ::_thesis: f /. i c= f /. j
consider k being Nat such that
A5: i + k = j by A2, NAT_1:10;
defpred S1[ Element of NAT ] means ( i + $1 <= j implies f /. i c= f /. (i + $1) );
A6: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
A7: (i + k) + 1 = i + (k + 1) ;
assume A8: S1[k] ; ::_thesis: S1[k + 1]
thus S1[k + 1] ::_thesis: verum
proof
i + k >= i by NAT_1:11;
then A9: i + k >= 1 by A3, XXREAL_0:2;
assume A10: i + (k + 1) <= j ; ::_thesis: f /. i c= f /. (i + (k + 1))
then i + k < j by A7, NAT_1:13;
then i + k < len f by A4, XXREAL_0:2;
then f /. (i + k) c= f /. (i + (k + 1)) by A1, A7, A9;
hence f /. i c= f /. (i + (k + 1)) by A7, A8, A10, NAT_1:13, XBOOLE_1:1; ::_thesis: verum
end;
end;
A11: S1[ 0 ] ;
A12: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A11, A6);
k in NAT by ORDINAL1:def_12;
hence f /. i c= f /. j by A12, A5; ::_thesis: verum
end;
theorem Th2: :: FIN_TOPO:2
for A being set
for f being FinSequence of bool A st ( for i being Element of NAT st 1 <= i & i < len f holds
f /. i c= f /. (i + 1) ) holds
for i, j being Element of NAT st 1 <= i & j <= len f & f /. j c= f /. i holds
for k being Element of NAT st i <= k & k <= j holds
f /. j = f /. k
proof
let A be set ; ::_thesis: for f being FinSequence of bool A st ( for i being Element of NAT st 1 <= i & i < len f holds
f /. i c= f /. (i + 1) ) holds
for i, j being Element of NAT st 1 <= i & j <= len f & f /. j c= f /. i holds
for k being Element of NAT st i <= k & k <= j holds
f /. j = f /. k
let f be FinSequence of bool A; ::_thesis: ( ( for i being Element of NAT st 1 <= i & i < len f holds
f /. i c= f /. (i + 1) ) implies for i, j being Element of NAT st 1 <= i & j <= len f & f /. j c= f /. i holds
for k being Element of NAT st i <= k & k <= j holds
f /. j = f /. k )
assume A1: for i being Element of NAT st 1 <= i & i < len f holds
f /. i c= f /. (i + 1) ; ::_thesis: for i, j being Element of NAT st 1 <= i & j <= len f & f /. j c= f /. i holds
for k being Element of NAT st i <= k & k <= j holds
f /. j = f /. k
let i, j be Element of NAT ; ::_thesis: ( 1 <= i & j <= len f & f /. j c= f /. i implies for k being Element of NAT st i <= k & k <= j holds
f /. j = f /. k )
assume that
A2: 1 <= i and
A3: j <= len f and
A4: f /. j c= f /. i ; ::_thesis: for k being Element of NAT st i <= k & k <= j holds
f /. j = f /. k
let k be Element of NAT ; ::_thesis: ( i <= k & k <= j implies f /. j = f /. k )
assume that
A5: i <= k and
A6: k <= j ; ::_thesis: f /. j = f /. k
1 <= k by A2, A5, XXREAL_0:2;
then A7: f /. k c= f /. j by A1, A3, A6, Th1;
defpred S1[ Element of NAT ] means ( i + $1 <= j implies f /. j c= f /. (i + $1) );
A8: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A9: S1[k] ; ::_thesis: S1[k + 1]
A10: (i + k) + 1 = i + (k + 1) ;
thus S1[k + 1] ::_thesis: verum
proof
i + k >= i by NAT_1:11;
then A11: i + k >= 1 by A2, XXREAL_0:2;
assume A12: i + (k + 1) <= j ; ::_thesis: f /. j c= f /. (i + (k + 1))
then i + k < j by A10, NAT_1:13;
then i + k < len f by A3, XXREAL_0:2;
then f /. (i + k) c= f /. ((i + k) + 1) by A1, A11;
hence f /. j c= f /. (i + (k + 1)) by A9, A12, NAT_1:13, XBOOLE_1:1; ::_thesis: verum
end;
end;
A13: S1[ 0 ] by A4;
A14: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A13, A8);
consider m being Nat such that
A15: k = i + m by A5, NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
k = i + m by A15;
then f /. j c= f /. k by A14, A6;
hence f /. j = f /. k by A7, XBOOLE_0:def_10; ::_thesis: verum
end;
scheme :: FIN_TOPO:sch 1
MaxFinSeqEx{ F1() -> non empty set , F2() -> Subset of F1(), F3() -> Subset of F1(), F4( Subset of F1()) -> Subset of F1() } :
ex f being FinSequence of bool F1() st
( len f > 0 & f /. 1 = F3() & ( for i being Element of NAT st i > 0 & i < len f holds
f /. (i + 1) = F4((f /. i)) ) & F4((f /. (len f))) = f /. (len f) & ( for i, j being Element of NAT st i > 0 & i < j & j <= len f holds
( f /. i c= F2() & f /. i c< f /. j ) ) )
provided
A1: F2() is finite and
A2: F3() c= F2() and
A3: for A being Subset of F1() st A c= F2() holds
( A c= F4(A) & F4(A) c= F2() )
proof
deffunc H1( Nat, Subset of F1()) -> Subset of F1() = F4($2);
consider f being Function of NAT,(bool F1()) such that
A4: f . 0 = F3() and
A5: for n being Nat holds f . (n + 1) = H1(n,f . n) from NAT_1:sch_12();
defpred S1[ Nat] means f . $1 c= F2();
A6: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
S1[n_+_1]
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A7: S1[n] ; ::_thesis: S1[n + 1]
f . (n + 1) = F4((f . n)) by A5;
hence S1[n + 1] by A3, A7; ::_thesis: verum
end;
A8: S1[ 0 ] by A2, A4;
A9: for n being Element of NAT holds S1[n] from NAT_1:sch_1(A8, A6);
A10: for i being Element of NAT holds f . i c= f . (i + 1)
proof
let i be Element of NAT ; ::_thesis: f . i c= f . (i + 1)
( f . (i + 1) = F4((f . i)) & f . i c= F2() ) by A5, A9;
hence f . i c= f . (i + 1) by A3; ::_thesis: verum
end;
A11: dom f = NAT by FUNCT_2:def_1;
A12: rng f is c=-linear
proof
let B, C be set ; :: according to ORDINAL1:def_8 ::_thesis: ( not B in rng f or not C in rng f or B,C are_c=-comparable )
assume B in rng f ; ::_thesis: ( not C in rng f or B,C are_c=-comparable )
then consider i being set such that
A13: i in NAT and
A14: B = f . i by A11, FUNCT_1:def_3;
reconsider i = i as Element of NAT by A13;
assume C in rng f ; ::_thesis: B,C are_c=-comparable
then consider j being set such that
A15: j in NAT and
A16: C = f . j by A11, FUNCT_1:def_3;
reconsider j = j as Element of NAT by A15;
( i <= j or j <= i ) ;
hence ( B c= C or C c= B ) by A10, A14, A16, MEASURE2:18; :: according to XBOOLE_0:def_9 ::_thesis: verum
end;
A17: rng f c= bool F2()
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in bool F2() )
assume x in rng f ; ::_thesis: x in bool F2()
then x in f .: NAT by RELSET_1:22;
then ex k being Element of NAT st
( k in NAT & f . k = x ) by FUNCT_2:65;
then x c= F2() by A9;
hence x in bool F2() ; ::_thesis: verum
end;
rng f <> {} by A4, A11, FUNCT_1:def_3;
then consider m being set such that
A18: m in rng f and
A19: for C being set st C in rng f holds
C c= m by A1, A17, A12, FINSET_1:12;
deffunc H2( Nat) -> Element of bool F1() = f . (abs ($1 - 1));
defpred S2[ set ] means ( $1 in NAT & f . $1 = m );
m in f .: NAT by A18, RELSET_1:22;
then ex k being Element of NAT st S2[k] by FUNCT_2:65;
then A20: ex k being Nat st S2[k] ;
consider k being Nat such that
A21: S2[k] and
A22: for n being Nat st S2[n] holds
k <= n from NAT_1:sch_5(A20);
consider z being FinSequence of bool F1() such that
A23: len z = k + 1 and
A24: for j being Nat st j in dom z holds
z . j = H2(j) from FINSEQ_2:sch_1();
A25: 0 + 1 <= len z by A23, NAT_1:13;
then A26: 1 in Seg (k + 1) by A23, FINSEQ_1:1;
take z ; ::_thesis: ( len z > 0 & z /. 1 = F3() & ( for i being Element of NAT st i > 0 & i < len z holds
z /. (i + 1) = F4((z /. i)) ) & F4((z /. (len z))) = z /. (len z) & ( for i, j being Element of NAT st i > 0 & i < j & j <= len z holds
( z /. i c= F2() & z /. i c< z /. j ) ) )
thus 0 < len z by A23; ::_thesis: ( z /. 1 = F3() & ( for i being Element of NAT st i > 0 & i < len z holds
z /. (i + 1) = F4((z /. i)) ) & F4((z /. (len z))) = z /. (len z) & ( for i, j being Element of NAT st i > 0 & i < j & j <= len z holds
( z /. i c= F2() & z /. i c< z /. j ) ) )
A27: dom z = Seg (k + 1) by A23, FINSEQ_1:def_3;
thus z /. 1 = z . 1 by A25, FINSEQ_4:15
.= f . (abs (1 - 1)) by A24, A27, A26
.= F3() by A4, ABSVALUE:2 ; ::_thesis: ( ( for i being Element of NAT st i > 0 & i < len z holds
z /. (i + 1) = F4((z /. i)) ) & F4((z /. (len z))) = z /. (len z) & ( for i, j being Element of NAT st i > 0 & i < j & j <= len z holds
( z /. i c= F2() & z /. i c< z /. j ) ) )
thus A28: for i being Element of NAT st i > 0 & i < len z holds
z /. (i + 1) = F4((z /. i)) ::_thesis: ( F4((z /. (len z))) = z /. (len z) & ( for i, j being Element of NAT st i > 0 & i < j & j <= len z holds
( z /. i c= F2() & z /. i c< z /. j ) ) )
proof
let i be Element of NAT ; ::_thesis: ( i > 0 & i < len z implies z /. (i + 1) = F4((z /. i)) )
assume that
A29: i > 0 and
A30: i < len z ; ::_thesis: z /. (i + 1) = F4((z /. i))
A31: ( 0 + 1 < i + 1 & i + 1 <= k + 1 ) by A23, A29, A30, NAT_1:13, XREAL_1:6;
then A32: i + 1 in Seg (k + 1) by FINSEQ_1:1;
A33: 0 + 1 <= i by A29, NAT_1:13;
then i in Seg (k + 1) by A23, A30, FINSEQ_1:1;
then A34: ( z . i = f . (abs (i - 1)) & i in dom z ) by A24, A27;
1 - 1 <= i - 1 by A33, XREAL_1:9;
then A35: 0 <= (i - 1) * 1 ;
thus z /. (i + 1) = z . (i + 1) by A23, A31, FINSEQ_4:15
.= f . (abs ((i + 1) - 1)) by A24, A27, A32
.= f . (abs ((i - 1) + 1))
.= f . ((abs (i - 1)) + (abs 1)) by A35, ABSVALUE:11
.= f . ((abs (i - 1)) + 1) by ABSVALUE:def_1
.= F4((f . (abs (i - 1)))) by A5
.= F4((z /. i)) by A34, PARTFUN1:def_6 ; ::_thesis: verum
end;
thus F4((z /. (len z))) = z /. (len z) ::_thesis: for i, j being Element of NAT st i > 0 & i < j & j <= len z holds
( z /. i c= F2() & z /. i c< z /. j )
proof
k + 1 in NAT ;
then k + 1 in dom f by FUNCT_2:def_1;
then f . (k + 1) in rng f by FUNCT_1:def_3;
then A36: f . (k + 1) c= f . k by A19, A21;
reconsider k9 = k as Element of NAT by ORDINAL1:def_12;
k in NAT by ORDINAL1:def_12;
then A37: f . k c= f . (k + 1) by A10;
( len z = 0 or len z in Seg (len z) ) by FINSEQ_1:3;
then A38: len z in dom z by A23, FINSEQ_1:def_3;
A39: z . (len z) = f . (abs ((k + 1) - 1)) by A23, A24, A27, FINSEQ_1:3
.= f . k by ABSVALUE:def_1 ;
hence F4((z /. (len z))) = F4((f . k9)) by A38, PARTFUN1:def_6
.= f . (k + 1) by A5
.= z . (len z) by A37, A36, A39, XBOOLE_0:def_10
.= z /. (len z) by A38, PARTFUN1:def_6 ;
::_thesis: verum
end;
let i, j be Element of NAT ; ::_thesis: ( i > 0 & i < j & j <= len z implies ( z /. i c= F2() & z /. i c< z /. j ) )
assume that
A40: 0 < i and
A41: i < j and
A42: j <= len z ; ::_thesis: ( z /. i c= F2() & z /. i c< z /. j )
A43: 0 + 1 <= i by A40, NAT_1:13;
then reconsider l = i - 1 as Element of NAT by INT_1:5;
A44: i <= len z by A41, A42, XXREAL_0:2;
then A45: i in Seg (k + 1) by A23, A43, FINSEQ_1:1;
A46: z /. i = z . i by A43, A44, FINSEQ_4:15
.= f . (abs (i - 1)) by A24, A27, A45
.= f . l by ABSVALUE:def_1 ;
hence z /. i c= F2() by A9; ::_thesis: z /. i c< z /. j
A47: for i being Element of NAT st 1 <= i & i < len z holds
z /. i c= z /. (i + 1)
proof
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len z implies z /. i c= z /. (i + 1) )
assume that
A48: 1 <= i and
A49: i < len z ; ::_thesis: z /. i c= z /. (i + 1)
A50: i in Seg (k + 1) by A23, A48, A49, FINSEQ_1:1;
A51: 1 - 1 <= i - 1 by A48, XREAL_1:9;
then A52: i - 1 is Element of NAT by INT_1:3;
A53: ( 1 <= i + 1 & i + 1 <= len z ) by A48, A49, NAT_1:13;
then A54: i + 1 in Seg (k + 1) by A23, FINSEQ_1:1;
A55: z /. (i + 1) = z . (i + 1) by A53, FINSEQ_4:15
.= f . (abs ((i + 1) - 1)) by A24, A27, A54
.= f . ((i - 1) + 1) by ABSVALUE:def_1 ;
z /. i = z . i by A48, A49, FINSEQ_4:15
.= f . (abs (i - 1)) by A24, A27, A50
.= f . (i - 1) by A51, ABSVALUE:def_1 ;
hence z /. i c= z /. (i + 1) by A10, A55, A52; ::_thesis: verum
end;
hence z /. i c= z /. j by A41, A42, A43, Th1; :: according to XBOOLE_0:def_8 ::_thesis: not z /. i = z /. j
defpred S3[ Element of NAT ] means ( i + $1 <= len z implies z /. i = z /. (i + $1) );
A56: ( i <= i + 1 & i + 1 <= j ) by A41, NAT_1:13;
k + 1 in Seg (k + 1) by FINSEQ_1:4;
then A57: k + 1 in dom z by A23, FINSEQ_1:def_3;
A58: i < len z by A41, A42, XXREAL_0:2;
assume z /. i = z /. j ; ::_thesis: contradiction
then A59: z /. i = z /. (i + 1) by A42, A43, A47, A56, Th2
.= F4((z /. i)) by A28, A40, A58 ;
A60: now__::_thesis:_for_n_being_Element_of_NAT_st_S3[n]_holds_
S3[n_+_1]
let n be Element of NAT ; ::_thesis: ( S3[n] implies S3[n + 1] )
assume A61: S3[n] ; ::_thesis: S3[n + 1]
thus S3[n + 1] ::_thesis: verum
proof
assume i + (n + 1) <= len z ; ::_thesis: z /. i = z /. (i + (n + 1))
then (i + n) + 1 <= len z ;
then i + n < len z by NAT_1:13;
hence z /. i = z /. ((i + n) + 1) by A28, A40, A59, A61
.= z /. (i + (n + 1)) ;
::_thesis: verum
end;
end;
consider n0 being Nat such that
A62: i + n0 = len z by A41, A42, NAT_1:10, XXREAL_0:2;
reconsider n0 = n0 as Element of NAT by ORDINAL1:def_12;
A63: i + n0 = len z by A62;
A64: S3[ 0 ] ;
for n being Element of NAT holds S3[n] from NAT_1:sch_1(A64, A60);
then f . l = z /. (k + 1) by A23, A46, A63
.= z . (k + 1) by A57, PARTFUN1:def_6
.= f . (abs ((k + 1) - 1)) by A24, A27, FINSEQ_1:4
.= m by A21, ABSVALUE:def_1 ;
then k <= l by A22;
then len z <= l + 1 by A23, XREAL_1:6;
hence contradiction by A41, A42, XXREAL_0:2; ::_thesis: verum
end;
registration
cluster non empty strict for RelStr ;
existence
ex b1 being RelStr st
( not b1 is empty & b1 is strict )
proof
set D = the non empty set ;
set f = the Relation of the non empty set ;
take RelStr(# the non empty set , the Relation of the non empty set #) ; ::_thesis: ( not RelStr(# the non empty set , the Relation of the non empty set #) is empty & RelStr(# the non empty set , the Relation of the non empty set #) is strict )
thus not the carrier of RelStr(# the non empty set , the Relation of the non empty set #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: RelStr(# the non empty set , the Relation of the non empty set #) is strict
thus RelStr(# the non empty set , the Relation of the non empty set #) is strict ; ::_thesis: verum
end;
end;
definition
let FT be RelStr ;
let x be Element of FT;
func U_FT x -> Subset of FT equals :: FIN_TOPO:def 1
Class ( the InternalRel of FT,x);
coherence
Class ( the InternalRel of FT,x) is Subset of FT ;
end;
:: deftheorem defines U_FT FIN_TOPO:def_1_:_
for FT being RelStr
for x being Element of FT holds U_FT x = Class ( the InternalRel of FT,x);
definition
let x be set ;
let y be Subset of {x};
:: original: .-->
redefine funcx .--> y -> Function of {x},(bool {x});
coherence
x .--> y is Function of {x},(bool {x})
proof
A1: dom (x .--> y) = {x} by FUNCOP_1:13;
rng (x .--> y) = {y} by FUNCOP_1:8;
then reconsider R = x .--> y as Relation of {x},(bool {x}) by A1, RELSET_1:4;
R is quasi_total by A1, FUNCT_2:def_1;
hence x .--> y is Function of {x},(bool {x}) ; ::_thesis: verum
end;
end;
definition
let x be set ;
func SinglRel x -> Relation of {x} equals :: FIN_TOPO:def 2
{[x,x]};
coherence
{[x,x]} is Relation of {x}
proof
x in {x} by TARSKI:def_1;
hence {[x,x]} is Relation of {x} by RELSET_1:3; ::_thesis: verum
end;
end;
:: deftheorem defines SinglRel FIN_TOPO:def_2_:_
for x being set holds SinglRel x = {[x,x]};
definition
func FT{0} -> strict RelStr equals :: FIN_TOPO:def 3
RelStr(# {0},(SinglRel 0) #);
coherence
RelStr(# {0},(SinglRel 0) #) is strict RelStr ;
end;
:: deftheorem defines FT{0} FIN_TOPO:def_3_:_
FT{0} = RelStr(# {0},(SinglRel 0) #);
registration
cluster FT{0} -> non empty strict ;
coherence
not FT{0} is empty ;
end;
notation
let IT be non empty RelStr ;
synonym filled IT for reflexive ;
end;
definition
let IT be non empty RelStr ;
redefine attr IT is reflexive means :Def4: :: FIN_TOPO:def 4
for x being Element of IT holds x in U_FT x;
compatibility
( IT is filled iff for x being Element of IT holds x in U_FT x )
proof
thus ( IT is filled implies for x being Element of IT holds x in U_FT x ) ::_thesis: ( ( for x being Element of IT holds x in U_FT x ) implies IT is filled )
proof
assume A1: IT is filled ; ::_thesis: for x being Element of IT holds x in U_FT x
let x be Element of IT; ::_thesis: x in U_FT x
x <= x by A1, ORDERS_2:1;
then [x,x] in the InternalRel of IT by ORDERS_2:def_5;
hence x in U_FT x by EQREL_1:18; ::_thesis: verum
end;
assume A2: for x being Element of IT holds x in U_FT x ; ::_thesis: IT is filled
let x be set ; :: according to RELAT_2:def_1,ORDERS_2:def_2 ::_thesis: ( not x in the carrier of IT or [x,x] in the InternalRel of IT )
assume x in the carrier of IT ; ::_thesis: [x,x] in the InternalRel of IT
then reconsider x = x as Element of IT ;
x in U_FT x by A2;
hence [x,x] in the InternalRel of IT by EQREL_1:18; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines filled FIN_TOPO:def_4_:_
for IT being non empty RelStr holds
( IT is filled iff for x being Element of IT holds x in U_FT x );
theorem Th3: :: FIN_TOPO:3
FT{0} is filled
proof
let x be Element of FT{0}; :: according to FIN_TOPO:def_4 ::_thesis: x in U_FT x
( x = 0 & [0,0] in SinglRel 0 ) by TARSKI:def_1;
hence x in U_FT x by RELAT_1:def_13; ::_thesis: verum
end;
registration
cluster FT{0} -> finite strict filled ;
coherence
( FT{0} is filled & FT{0} is finite ) by Th3;
end;
registration
cluster non empty finite strict filled for RelStr ;
existence
ex b1 being non empty RelStr st
( b1 is finite & b1 is filled & b1 is strict ) by Th3;
end;
theorem :: FIN_TOPO:4
for FT being non empty filled RelStr holds { (U_FT x) where x is Element of FT : verum } is Cover of FT
proof
let FT be non empty filled RelStr ; ::_thesis: { (U_FT x) where x is Element of FT : verum } is Cover of FT
let a be set ; :: according to TARSKI:def_3,SETFAM_1:def_11 ::_thesis: ( not a in the carrier of FT or a in union { (U_FT x) where x is Element of FT : verum } )
assume a in the carrier of FT ; ::_thesis: a in union { (U_FT x) where x is Element of FT : verum }
then reconsider b = a as Element of FT ;
( b in U_FT b & U_FT b in { (U_FT x) where x is Element of FT : verum } ) by Def4;
hence a in union { (U_FT x) where x is Element of FT : verum } by TARSKI:def_4; ::_thesis: verum
end;
definition
let FT be non empty RelStr ;
let A be Subset of FT;
funcA ^delta -> Subset of FT equals :: FIN_TOPO:def 5
{ x where x is Element of FT : ( U_FT x meets A & U_FT x meets A ` ) } ;
coherence
{ x where x is Element of FT : ( U_FT x meets A & U_FT x meets A ` ) } is Subset of FT
proof
defpred S1[ Element of FT] means ( U_FT $1 meets A & U_FT $1 meets A ` );
{ x where x is Element of FT : S1[x] } is Subset of FT from DOMAIN_1:sch_7();
hence { x where x is Element of FT : ( U_FT x meets A & U_FT x meets A ` ) } is Subset of FT ; ::_thesis: verum
end;
end;
:: deftheorem defines ^delta FIN_TOPO:def_5_:_
for FT being non empty RelStr
for A being Subset of FT holds A ^delta = { x where x is Element of FT : ( U_FT x meets A & U_FT x meets A ` ) } ;
theorem Th5: :: FIN_TOPO:5
for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT holds
( x in A ^delta iff ( U_FT x meets A & U_FT x meets A ` ) )
proof
let FT be non empty RelStr ; ::_thesis: for x being Element of FT
for A being Subset of FT holds
( x in A ^delta iff ( U_FT x meets A & U_FT x meets A ` ) )
let x be Element of FT; ::_thesis: for A being Subset of FT holds
( x in A ^delta iff ( U_FT x meets A & U_FT x meets A ` ) )
let A be Subset of FT; ::_thesis: ( x in A ^delta iff ( U_FT x meets A & U_FT x meets A ` ) )
thus ( x in A ^delta implies ( U_FT x meets A & U_FT x meets A ` ) ) ::_thesis: ( U_FT x meets A & U_FT x meets A ` implies x in A ^delta )
proof
assume x in A ^delta ; ::_thesis: ( U_FT x meets A & U_FT x meets A ` )
then ex y being Element of FT st
( y = x & U_FT y meets A & U_FT y meets A ` ) ;
hence ( U_FT x meets A & U_FT x meets A ` ) ; ::_thesis: verum
end;
assume ( U_FT x meets A & U_FT x meets A ` ) ; ::_thesis: x in A ^delta
hence x in A ^delta ; ::_thesis: verum
end;
definition
let FT be non empty RelStr ;
let A be Subset of FT;
funcA ^deltai -> Subset of FT equals :: FIN_TOPO:def 6
A /\ (A ^delta);
coherence
A /\ (A ^delta) is Subset of FT ;
funcA ^deltao -> Subset of FT equals :: FIN_TOPO:def 7
(A `) /\ (A ^delta);
coherence
(A `) /\ (A ^delta) is Subset of FT ;
end;
:: deftheorem defines ^deltai FIN_TOPO:def_6_:_
for FT being non empty RelStr
for A being Subset of FT holds A ^deltai = A /\ (A ^delta);
:: deftheorem defines ^deltao FIN_TOPO:def_7_:_
for FT being non empty RelStr
for A being Subset of FT holds A ^deltao = (A `) /\ (A ^delta);
theorem :: FIN_TOPO:6
for FT being non empty RelStr
for A being Subset of FT holds A ^delta = (A ^deltai) \/ (A ^deltao)
proof
let FT be non empty RelStr ; ::_thesis: for A being Subset of FT holds A ^delta = (A ^deltai) \/ (A ^deltao)
let A be Subset of FT; ::_thesis: A ^delta = (A ^deltai) \/ (A ^deltao)
for x being set holds
( x in A ^delta iff x in (A ^deltai) \/ (A ^deltao) )
proof
let x be set ; ::_thesis: ( x in A ^delta iff x in (A ^deltai) \/ (A ^deltao) )
thus ( x in A ^delta implies x in (A ^deltai) \/ (A ^deltao) ) ::_thesis: ( x in (A ^deltai) \/ (A ^deltao) implies x in A ^delta )
proof
assume x in A ^delta ; ::_thesis: x in (A ^deltai) \/ (A ^deltao)
then x in ([#] the carrier of FT) /\ (A ^delta) by XBOOLE_1:28;
then x in (A \/ (A `)) /\ (A ^delta) by SUBSET_1:10;
hence x in (A ^deltai) \/ (A ^deltao) by XBOOLE_1:23; ::_thesis: verum
end;
assume x in (A ^deltai) \/ (A ^deltao) ; ::_thesis: x in A ^delta
then x in (A \/ (A `)) /\ (A ^delta) by XBOOLE_1:23;
then x in ([#] the carrier of FT) /\ (A ^delta) by SUBSET_1:10;
hence x in A ^delta by XBOOLE_1:28; ::_thesis: verum
end;
hence A ^delta = (A ^deltai) \/ (A ^deltao) by TARSKI:1; ::_thesis: verum
end;
definition
let FT be non empty RelStr ;
let A be Subset of FT;
funcA ^i -> Subset of FT equals :: FIN_TOPO:def 8
{ x where x is Element of FT : U_FT x c= A } ;
coherence
{ x where x is Element of FT : U_FT x c= A } is Subset of FT
proof
defpred S1[ Element of FT] means U_FT $1 c= A;
{ x where x is Element of FT : S1[x] } is Subset of FT from DOMAIN_1:sch_7();
hence { x where x is Element of FT : U_FT x c= A } is Subset of FT ; ::_thesis: verum
end;
funcA ^b -> Subset of FT equals :: FIN_TOPO:def 9
{ x where x is Element of FT : U_FT x meets A } ;
coherence
{ x where x is Element of FT : U_FT x meets A } is Subset of FT
proof
defpred S1[ Element of FT] means U_FT $1 meets A;
{ x where x is Element of FT : S1[x] } is Subset of FT from DOMAIN_1:sch_7();
hence { x where x is Element of FT : U_FT x meets A } is Subset of FT ; ::_thesis: verum
end;
funcA ^s -> Subset of FT equals :: FIN_TOPO:def 10
{ x where x is Element of FT : ( x in A & (U_FT x) \ {x} misses A ) } ;
coherence
{ x where x is Element of FT : ( x in A & (U_FT x) \ {x} misses A ) } is Subset of FT
proof
defpred S1[ Element of FT] means ( $1 in A & (U_FT $1) \ {$1} misses A );
{ x where x is Element of FT : S1[x] } is Subset of FT from DOMAIN_1:sch_7();
hence { x where x is Element of FT : ( x in A & (U_FT x) \ {x} misses A ) } is Subset of FT ; ::_thesis: verum
end;
end;
:: deftheorem defines ^i FIN_TOPO:def_8_:_
for FT being non empty RelStr
for A being Subset of FT holds A ^i = { x where x is Element of FT : U_FT x c= A } ;
:: deftheorem defines ^b FIN_TOPO:def_9_:_
for FT being non empty RelStr
for A being Subset of FT holds A ^b = { x where x is Element of FT : U_FT x meets A } ;
:: deftheorem defines ^s FIN_TOPO:def_10_:_
for FT being non empty RelStr
for A being Subset of FT holds A ^s = { x where x is Element of FT : ( x in A & (U_FT x) \ {x} misses A ) } ;
definition
let FT be non empty RelStr ;
let A be Subset of FT;
funcA ^n -> Subset of FT equals :: FIN_TOPO:def 11
A \ (A ^s);
coherence
A \ (A ^s) is Subset of FT ;
funcA ^f -> Subset of FT equals :: FIN_TOPO:def 12
{ x where x is Element of FT : ex y being Element of FT st
( y in A & x in U_FT y ) } ;
coherence
{ x where x is Element of FT : ex y being Element of FT st
( y in A & x in U_FT y ) } is Subset of FT
proof
defpred S1[ Element of FT] means ex y being Element of FT st
( y in A & $1 in U_FT y );
{ x where x is Element of FT : S1[x] } is Subset of FT from DOMAIN_1:sch_7();
hence { x where x is Element of FT : ex y being Element of FT st
( y in A & x in U_FT y ) } is Subset of FT ; ::_thesis: verum
end;
end;
:: deftheorem defines ^n FIN_TOPO:def_11_:_
for FT being non empty RelStr
for A being Subset of FT holds A ^n = A \ (A ^s);
:: deftheorem defines ^f FIN_TOPO:def_12_:_
for FT being non empty RelStr
for A being Subset of FT holds A ^f = { x where x is Element of FT : ex y being Element of FT st
( y in A & x in U_FT y ) } ;
definition
let IT be non empty RelStr ;
attrIT is symmetric means :Def13: :: FIN_TOPO:def 13
for x, y being Element of IT st y in U_FT x holds
x in U_FT y;
end;
:: deftheorem Def13 defines symmetric FIN_TOPO:def_13_:_
for IT being non empty RelStr holds
( IT is symmetric iff for x, y being Element of IT st y in U_FT x holds
x in U_FT y );
theorem Th7: :: FIN_TOPO:7
for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT holds
( x in A ^i iff U_FT x c= A )
proof
let FT be non empty RelStr ; ::_thesis: for x being Element of FT
for A being Subset of FT holds
( x in A ^i iff U_FT x c= A )
let x be Element of FT; ::_thesis: for A being Subset of FT holds
( x in A ^i iff U_FT x c= A )
let A be Subset of FT; ::_thesis: ( x in A ^i iff U_FT x c= A )
thus ( x in A ^i implies U_FT x c= A ) ::_thesis: ( U_FT x c= A implies x in A ^i )
proof
assume x in A ^i ; ::_thesis: U_FT x c= A
then ex y being Element of FT st
( y = x & U_FT y c= A ) ;
hence U_FT x c= A ; ::_thesis: verum
end;
assume U_FT x c= A ; ::_thesis: x in A ^i
hence x in A ^i ; ::_thesis: verum
end;
theorem Th8: :: FIN_TOPO:8
for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT holds
( x in A ^b iff U_FT x meets A )
proof
let FT be non empty RelStr ; ::_thesis: for x being Element of FT
for A being Subset of FT holds
( x in A ^b iff U_FT x meets A )
let x be Element of FT; ::_thesis: for A being Subset of FT holds
( x in A ^b iff U_FT x meets A )
let A be Subset of FT; ::_thesis: ( x in A ^b iff U_FT x meets A )
thus ( x in A ^b implies U_FT x meets A ) ::_thesis: ( U_FT x meets A implies x in A ^b )
proof
assume x in A ^b ; ::_thesis: U_FT x meets A
then ex y being Element of FT st
( y = x & U_FT y meets A ) ;
hence U_FT x meets A ; ::_thesis: verum
end;
assume U_FT x meets A ; ::_thesis: x in A ^b
hence x in A ^b ; ::_thesis: verum
end;
theorem Th9: :: FIN_TOPO:9
for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT holds
( x in A ^s iff ( x in A & (U_FT x) \ {x} misses A ) )
proof
let FT be non empty RelStr ; ::_thesis: for x being Element of FT
for A being Subset of FT holds
( x in A ^s iff ( x in A & (U_FT x) \ {x} misses A ) )
let x be Element of FT; ::_thesis: for A being Subset of FT holds
( x in A ^s iff ( x in A & (U_FT x) \ {x} misses A ) )
let A be Subset of FT; ::_thesis: ( x in A ^s iff ( x in A & (U_FT x) \ {x} misses A ) )
thus ( x in A ^s implies ( x in A & (U_FT x) \ {x} misses A ) ) ::_thesis: ( x in A & (U_FT x) \ {x} misses A implies x in A ^s )
proof
assume x in A ^s ; ::_thesis: ( x in A & (U_FT x) \ {x} misses A )
then ex y being Element of FT st
( y = x & y in A & (U_FT y) \ {y} misses A ) ;
hence ( x in A & (U_FT x) \ {x} misses A ) ; ::_thesis: verum
end;
assume ( x in A & (U_FT x) \ {x} misses A ) ; ::_thesis: x in A ^s
hence x in A ^s ; ::_thesis: verum
end;
theorem :: FIN_TOPO:10
for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT holds
( x in A ^n iff ( x in A & (U_FT x) \ {x} meets A ) )
proof
let FT be non empty RelStr ; ::_thesis: for x being Element of FT
for A being Subset of FT holds
( x in A ^n iff ( x in A & (U_FT x) \ {x} meets A ) )
let x be Element of FT; ::_thesis: for A being Subset of FT holds
( x in A ^n iff ( x in A & (U_FT x) \ {x} meets A ) )
let A be Subset of FT; ::_thesis: ( x in A ^n iff ( x in A & (U_FT x) \ {x} meets A ) )
thus ( x in A ^n implies ( x in A & (U_FT x) \ {x} meets A ) ) ::_thesis: ( x in A & (U_FT x) \ {x} meets A implies x in A ^n )
proof
assume x in A ^n ; ::_thesis: ( x in A & (U_FT x) \ {x} meets A )
then ( x in A & not x in A ^s ) by XBOOLE_0:def_5;
hence ( x in A & (U_FT x) \ {x} meets A ) ; ::_thesis: verum
end;
assume that
A1: x in A and
A2: (U_FT x) \ {x} meets A ; ::_thesis: x in A ^n
not x in A ^s by A2, Th9;
hence x in A ^n by A1, XBOOLE_0:def_5; ::_thesis: verum
end;
theorem Th11: :: FIN_TOPO:11
for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT holds
( x in A ^f iff ex y being Element of FT st
( y in A & x in U_FT y ) )
proof
let FT be non empty RelStr ; ::_thesis: for x being Element of FT
for A being Subset of FT holds
( x in A ^f iff ex y being Element of FT st
( y in A & x in U_FT y ) )
let x be Element of FT; ::_thesis: for A being Subset of FT holds
( x in A ^f iff ex y being Element of FT st
( y in A & x in U_FT y ) )
let A be Subset of FT; ::_thesis: ( x in A ^f iff ex y being Element of FT st
( y in A & x in U_FT y ) )
thus ( x in A ^f implies ex y being Element of FT st
( y in A & x in U_FT y ) ) ::_thesis: ( ex y being Element of FT st
( y in A & x in U_FT y ) implies x in A ^f )
proof
assume x in A ^f ; ::_thesis: ex y being Element of FT st
( y in A & x in U_FT y )
then ex y being Element of FT st
( y = x & ex z being Element of FT st
( z in A & y in U_FT z ) ) ;
hence ex y being Element of FT st
( y in A & x in U_FT y ) ; ::_thesis: verum
end;
assume ex z being Element of FT st
( z in A & x in U_FT z ) ; ::_thesis: x in A ^f
hence x in A ^f ; ::_thesis: verum
end;
theorem :: FIN_TOPO:12
for FT being non empty RelStr holds
( FT is symmetric iff for A being Subset of FT holds A ^b = A ^f )
proof
let FT be non empty RelStr ; ::_thesis: ( FT is symmetric iff for A being Subset of FT holds A ^b = A ^f )
thus ( FT is symmetric implies for A being Subset of FT holds A ^b = A ^f ) ::_thesis: ( ( for A being Subset of FT holds A ^b = A ^f ) implies FT is symmetric )
proof
assume A1: FT is symmetric ; ::_thesis: for A being Subset of FT holds A ^b = A ^f
let A be Subset of FT; ::_thesis: A ^b = A ^f
thus A ^b c= A ^f :: according to XBOOLE_0:def_10 ::_thesis: A ^f c= A ^b
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A ^b or x in A ^f )
assume A2: x in A ^b ; ::_thesis: x in A ^f
then reconsider y = x as Element of FT ;
U_FT y meets A by A2, Th8;
then consider z being set such that
A3: z in (U_FT y) /\ A by XBOOLE_0:4;
reconsider z = z as Element of FT by A3;
z in U_FT y by A3, XBOOLE_0:def_4;
then A4: y in U_FT z by A1, Def13;
z in A by A3, XBOOLE_0:def_4;
hence x in A ^f by A4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A ^f or x in A ^b )
assume A5: x in A ^f ; ::_thesis: x in A ^b
then reconsider y = x as Element of FT ;
consider z being Element of FT such that
A6: z in A and
A7: y in U_FT z by A5, Th11;
z in U_FT y by A1, A7, Def13;
then U_FT y meets A by A6, XBOOLE_0:3;
hence x in A ^b ; ::_thesis: verum
end;
assume A8: for A being Subset of FT holds A ^b = A ^f ; ::_thesis: FT is symmetric
let x, y be Element of FT; :: according to FIN_TOPO:def_13 ::_thesis: ( y in U_FT x implies x in U_FT y )
assume y in U_FT x ; ::_thesis: x in U_FT y
then U_FT x meets {y} by ZFMISC_1:48;
then x in {y} ^b ;
then x in {y} ^f by A8;
then ex z being Element of FT st
( z in {y} & x in U_FT z ) by Th11;
hence x in U_FT y by TARSKI:def_1; ::_thesis: verum
end;
definition
let FT be non empty RelStr ;
let IT be Subset of FT;
attrIT is open means :Def14: :: FIN_TOPO:def 14
IT = IT ^i ;
attrIT is closed means :Def15: :: FIN_TOPO:def 15
IT = IT ^b ;
attrIT is connected means :Def16: :: FIN_TOPO:def 16
for B, C being Subset of FT st IT = B \/ C & B <> {} & C <> {} & B misses C holds
B ^b meets C;
end;
:: deftheorem Def14 defines open FIN_TOPO:def_14_:_
for FT being non empty RelStr
for IT being Subset of FT holds
( IT is open iff IT = IT ^i );
:: deftheorem Def15 defines closed FIN_TOPO:def_15_:_
for FT being non empty RelStr
for IT being Subset of FT holds
( IT is closed iff IT = IT ^b );
:: deftheorem Def16 defines connected FIN_TOPO:def_16_:_
for FT being non empty RelStr
for IT being Subset of FT holds
( IT is connected iff for B, C being Subset of FT st IT = B \/ C & B <> {} & C <> {} & B misses C holds
B ^b meets C );
definition
let FT be non empty RelStr ;
let A be Subset of FT;
funcA ^fb -> Subset of FT equals :: FIN_TOPO:def 17
meet { F where F is Subset of FT : ( A c= F & F is closed ) } ;
coherence
meet { F where F is Subset of FT : ( A c= F & F is closed ) } is Subset of FT
proof
set FF = { F where F is Subset of FT : ( A c= F & F is closed ) } ;
{ F where F is Subset of FT : ( A c= F & F is closed ) } c= bool the carrier of FT
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { F where F is Subset of FT : ( A c= F & F is closed ) } or x in bool the carrier of FT )
assume x in { F where F is Subset of FT : ( A c= F & F is closed ) } ; ::_thesis: x in bool the carrier of FT
then ex F being Subset of FT st
( x = F & A c= F & F is closed ) ;
hence x in bool the carrier of FT ; ::_thesis: verum
end;
then reconsider FF = { F where F is Subset of FT : ( A c= F & F is closed ) } as Subset-Family of FT ;
meet FF is Subset of FT ;
hence meet { F where F is Subset of FT : ( A c= F & F is closed ) } is Subset of FT ; ::_thesis: verum
end;
funcA ^fi -> Subset of FT equals :: FIN_TOPO:def 18
union { F where F is Subset of FT : ( A c= F & F is open ) } ;
coherence
union { F where F is Subset of FT : ( A c= F & F is open ) } is Subset of FT
proof
set FF = { F where F is Subset of FT : ( A c= F & F is open ) } ;
{ F where F is Subset of FT : ( A c= F & F is open ) } c= bool the carrier of FT
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { F where F is Subset of FT : ( A c= F & F is open ) } or x in bool the carrier of FT )
assume x in { F where F is Subset of FT : ( A c= F & F is open ) } ; ::_thesis: x in bool the carrier of FT
then ex F being Subset of FT st
( x = F & A c= F & F is open ) ;
hence x in bool the carrier of FT ; ::_thesis: verum
end;
then reconsider FF = { F where F is Subset of FT : ( A c= F & F is open ) } as Subset-Family of FT ;
union FF is Subset of FT ;
hence union { F where F is Subset of FT : ( A c= F & F is open ) } is Subset of FT ; ::_thesis: verum
end;
end;
:: deftheorem defines ^fb FIN_TOPO:def_17_:_
for FT being non empty RelStr
for A being Subset of FT holds A ^fb = meet { F where F is Subset of FT : ( A c= F & F is closed ) } ;
:: deftheorem defines ^fi FIN_TOPO:def_18_:_
for FT being non empty RelStr
for A being Subset of FT holds A ^fi = union { F where F is Subset of FT : ( A c= F & F is open ) } ;
theorem Th13: :: FIN_TOPO:13
for FT being non empty filled RelStr
for A being Subset of FT holds A c= A ^b
proof
let FT be non empty filled RelStr ; ::_thesis: for A being Subset of FT holds A c= A ^b
let A be Subset of FT; ::_thesis: A c= A ^b
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in A ^b )
assume A1: x in A ; ::_thesis: x in A ^b
then reconsider y = x as Element of FT ;
y in U_FT y by Def4;
then U_FT y meets A by A1, XBOOLE_0:3;
hence x in A ^b ; ::_thesis: verum
end;
theorem Th14: :: FIN_TOPO:14
for FT being non empty RelStr
for A, B being Subset of FT st A c= B holds
A ^b c= B ^b
proof
let FT be non empty RelStr ; ::_thesis: for A, B being Subset of FT st A c= B holds
A ^b c= B ^b
let A, B be Subset of FT; ::_thesis: ( A c= B implies A ^b c= B ^b )
assume A1: A c= B ; ::_thesis: A ^b c= B ^b
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A ^b or x in B ^b )
assume A2: x in A ^b ; ::_thesis: x in B ^b
then reconsider y = x as Element of FT ;
U_FT y meets A by A2, Th8;
then ex w being set st
( w in U_FT y & w in A ) by XBOOLE_0:3;
then U_FT y meets B by A1, XBOOLE_0:3;
hence x in B ^b ; ::_thesis: verum
end;
theorem :: FIN_TOPO:15
for FT being non empty finite filled RelStr
for A being Subset of FT holds
( A is connected iff for x being Element of FT st x in A holds
ex S being FinSequence of bool the carrier of FT st
( len S > 0 & S /. 1 = {x} & ( for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A ) & A c= S /. (len S) ) )
proof
let FT be non empty finite filled RelStr ; ::_thesis: for A being Subset of FT holds
( A is connected iff for x being Element of FT st x in A holds
ex S being FinSequence of bool the carrier of FT st
( len S > 0 & S /. 1 = {x} & ( for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A ) & A c= S /. (len S) ) )
let A be Subset of FT; ::_thesis: ( A is connected iff for x being Element of FT st x in A holds
ex S being FinSequence of bool the carrier of FT st
( len S > 0 & S /. 1 = {x} & ( for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A ) & A c= S /. (len S) ) )
thus ( A is connected implies for x being Element of FT st x in A holds
ex S being FinSequence of bool the carrier of FT st
( len S > 0 & S /. 1 = {x} & ( for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A ) & A c= S /. (len S) ) ) ::_thesis: ( ( for x being Element of FT st x in A holds
ex S being FinSequence of bool the carrier of FT st
( len S > 0 & S /. 1 = {x} & ( for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A ) & A c= S /. (len S) ) ) implies A is connected )
proof
deffunc H1( Subset of FT) -> Element of K32( the carrier of FT) = ($1 ^b) /\ A;
assume A1: A is connected ; ::_thesis: for x being Element of FT st x in A holds
ex S being FinSequence of bool the carrier of FT st
( len S > 0 & S /. 1 = {x} & ( for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A ) & A c= S /. (len S) )
let x be Element of FT; ::_thesis: ( x in A implies ex S being FinSequence of bool the carrier of FT st
( len S > 0 & S /. 1 = {x} & ( for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A ) & A c= S /. (len S) ) )
assume x in A ; ::_thesis: ex S being FinSequence of bool the carrier of FT st
( len S > 0 & S /. 1 = {x} & ( for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A ) & A c= S /. (len S) )
then A2: {x} c= A by ZFMISC_1:31;
A3: for B being Subset of FT st B c= A holds
( B c= H1(B) & H1(B) c= A )
proof
let B be Subset of FT; ::_thesis: ( B c= A implies ( B c= H1(B) & H1(B) c= A ) )
assume A4: B c= A ; ::_thesis: ( B c= H1(B) & H1(B) c= A )
B c= B ^b by Th13;
hence B c= (B ^b) /\ A by A4, XBOOLE_1:19; ::_thesis: H1(B) c= A
thus H1(B) c= A by XBOOLE_1:17; ::_thesis: verum
end;
A5: A is finite ;
consider S being FinSequence of bool the carrier of FT such that
A6: len S > 0 and
A7: S /. 1 = {x} and
A8: for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = H1(S /. i) and
A9: H1(S /. (len S)) = S /. (len S) and
A10: for i, j being Element of NAT st i > 0 & i < j & j <= len S holds
( S /. i c= A & S /. i c< S /. j ) from FIN_TOPO:sch_1(A5, A2, A3);
consider k being Nat such that
A11: len S = k + 1 by A6, NAT_1:6;
set B = S /. (len S);
set C = A \ (S /. (len S));
A12: S /. (len S) misses A \ (S /. (len S)) by XBOOLE_1:79;
defpred S1[ Element of NAT ] means ( $1 < len S implies S /. ($1 + 1) <> {} );
A13: now__::_thesis:_for_i_being_Element_of_NAT_st_S1[i]_holds_
S1[i_+_1]
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A14: S1[i] ; ::_thesis: S1[i + 1]
thus S1[i + 1] ::_thesis: verum
proof
assume A15: i + 1 < len S ; ::_thesis: S /. ((i + 1) + 1) <> {}
then ( i + 1 < (i + 1) + 1 & (i + 1) + 1 <= len S ) by NAT_1:13;
then S /. (i + 1) c< S /. ((i + 1) + 1) by A10;
then S /. (i + 1) c= S /. ((i + 1) + 1) by XBOOLE_0:def_8;
hence S /. ((i + 1) + 1) <> {} by A14, A15, NAT_1:13; ::_thesis: verum
end;
end;
A16: S1[ 0 ] by A7;
A17: for i being Element of NAT holds S1[i] from NAT_1:sch_1(A16, A13);
reconsider k = k as Element of NAT by ORDINAL1:def_12;
k < len S by A11, NAT_1:13;
then A18: S /. (len S) <> {} by A17, A11;
take S ; ::_thesis: ( len S > 0 & S /. 1 = {x} & ( for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A ) & A c= S /. (len S) )
thus len S > 0 by A6; ::_thesis: ( S /. 1 = {x} & ( for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A ) & A c= S /. (len S) )
thus S /. 1 = {x} by A7; ::_thesis: ( ( for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A ) & A c= S /. (len S) )
thus for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A by A8; ::_thesis: A c= S /. (len S)
assume not A c= S /. (len S) ; ::_thesis: contradiction
then A19: A \ (S /. (len S)) <> {} by XBOOLE_1:37;
((S /. (len S)) ^b) /\ (A \ (S /. (len S))) = ((S /. (len S)) ^b) /\ (A /\ (A \ (S /. (len S)))) by XBOOLE_1:28, XBOOLE_1:36
.= (S /. (len S)) /\ (A \ (S /. (len S))) by A9, XBOOLE_1:16
.= {} by A12, XBOOLE_0:def_7 ;
then A20: ( S /. (len S) misses A \ (S /. (len S)) & (S /. (len S)) ^b misses A \ (S /. (len S)) ) by XBOOLE_0:def_7, XBOOLE_1:79;
(S /. (len S)) \/ (A \ (S /. (len S))) = (S /. (len S)) \/ A by XBOOLE_1:39
.= A by A9, XBOOLE_1:12, XBOOLE_1:17 ;
hence contradiction by A1, A19, A18, A20, Def16; ::_thesis: verum
end;
assume A21: for x being Element of FT st x in A holds
ex S being FinSequence of bool the carrier of FT st
( len S > 0 & S /. 1 = {x} & ( for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A ) & A c= S /. (len S) ) ; ::_thesis: A is connected
given B, C being Subset of FT such that A22: A = B \/ C and
A23: B <> {} and
A24: C <> {} and
A25: B misses C and
A26: B ^b misses C ; :: according to FIN_TOPO:def_16 ::_thesis: contradiction
set x = the Element of B;
the Element of B in A by A22, A23, XBOOLE_0:def_3;
then consider S being FinSequence of bool the carrier of FT such that
A27: len S > 0 and
A28: S /. 1 = { the Element of B} and
A29: for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A and
A30: A c= S /. (len S) by A21;
consider k being Nat such that
A31: len S = k + 1 by A27, NAT_1:6;
defpred S1[ Element of NAT ] means ( $1 < len S implies S /. ($1 + 1) c= B );
(B ^b) /\ C = {} by A26, XBOOLE_0:def_7;
then A32: (B ^b) /\ A = ((B ^b) /\ B) \/ {} by A22, XBOOLE_1:23
.= B by Th13, XBOOLE_1:28 ;
A33: now__::_thesis:_for_i_being_Element_of_NAT_st_S1[i]_holds_
S1[i_+_1]
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A34: S1[i] ; ::_thesis: S1[i + 1]
thus S1[i + 1] ::_thesis: verum
proof
assume A35: i + 1 < len S ; ::_thesis: S /. ((i + 1) + 1) c= B
then (S /. (i + 1)) ^b c= B ^b by A34, Th14, NAT_1:13;
then ((S /. (i + 1)) ^b) /\ A c= (B ^b) /\ A by XBOOLE_1:26;
hence S /. ((i + 1) + 1) c= B by A32, A29, A35; ::_thesis: verum
end;
end;
A36: S1[ 0 ] by A23, A28, ZFMISC_1:31;
A37: for i being Element of NAT holds S1[i] from NAT_1:sch_1(A36, A33);
reconsider k = k as Element of NAT by ORDINAL1:def_12;
k < len S by A31, NAT_1:13;
then A38: S /. (len S) c= B by A37, A31;
A39: B c= A by A22, XBOOLE_1:7;
then S /. (len S) c= A by A38, XBOOLE_1:1;
then S /. (len S) = A by A30, XBOOLE_0:def_10;
then A40: A = B by A39, A38, XBOOLE_0:def_10;
B /\ C = {} by A25, XBOOLE_0:def_7;
hence contradiction by A22, A24, A40, XBOOLE_1:7, XBOOLE_1:28; ::_thesis: verum
end;
theorem Th16: :: FIN_TOPO:16
for FT being non empty RelStr
for A being Subset of FT holds ((A `) ^i) ` = A ^b
proof
let FT be non empty RelStr ; ::_thesis: for A being Subset of FT holds ((A `) ^i) ` = A ^b
let A be Subset of FT; ::_thesis: ((A `) ^i) ` = A ^b
for x being set holds
( x in ((A `) ^i) ` iff x in A ^b )
proof
let x be set ; ::_thesis: ( x in ((A `) ^i) ` iff x in A ^b )
thus ( x in ((A `) ^i) ` implies x in A ^b ) ::_thesis: ( x in A ^b implies x in ((A `) ^i) ` )
proof
assume A1: x in ((A `) ^i) ` ; ::_thesis: x in A ^b
then reconsider y = x as Element of FT ;
not y in (A `) ^i by A1, XBOOLE_0:def_5;
then not U_FT y c= A ` ;
then consider z being set such that
A2: z in U_FT y and
A3: not z in A ` by TARSKI:def_3;
z in A by A2, A3, SUBSET_1:29;
then U_FT y meets A by A2, XBOOLE_0:3;
hence x in A ^b ; ::_thesis: verum
end;
assume A4: x in A ^b ; ::_thesis: x in ((A `) ^i) `
then reconsider y = x as Element of FT ;
U_FT y meets A by A4, Th8;
then ex z being set st
( z in U_FT y & z in A ) by XBOOLE_0:3;
then not U_FT y c= A ` by XBOOLE_0:def_5;
then not y in (A `) ^i by Th7;
hence x in ((A `) ^i) ` by SUBSET_1:29; ::_thesis: verum
end;
hence ((A `) ^i) ` = A ^b by TARSKI:1; ::_thesis: verum
end;
theorem Th17: :: FIN_TOPO:17
for FT being non empty RelStr
for A being Subset of FT holds ((A `) ^b) ` = A ^i
proof
let FT be non empty RelStr ; ::_thesis: for A being Subset of FT holds ((A `) ^b) ` = A ^i
let A be Subset of FT; ::_thesis: ((A `) ^b) ` = A ^i
for x being set holds
( x in ((A `) ^b) ` iff x in A ^i )
proof
let x be set ; ::_thesis: ( x in ((A `) ^b) ` iff x in A ^i )
thus ( x in ((A `) ^b) ` implies x in A ^i ) ::_thesis: ( x in A ^i implies x in ((A `) ^b) ` )
proof
assume A1: x in ((A `) ^b) ` ; ::_thesis: x in A ^i
then reconsider y = x as Element of FT ;
not y in (A `) ^b by A1, XBOOLE_0:def_5;
then U_FT y misses A ` ;
then (U_FT y) /\ (A `) = {} by XBOOLE_0:def_7;
then (U_FT y) \ A = {} by SUBSET_1:13;
then U_FT y c= A by XBOOLE_1:37;
hence x in A ^i ; ::_thesis: verum
end;
assume A2: x in A ^i ; ::_thesis: x in ((A `) ^b) `
then reconsider y = x as Element of FT ;
U_FT y c= A by A2, Th7;
then (U_FT y) \ A = {} by XBOOLE_1:37;
then (U_FT y) /\ (A `) = {} by SUBSET_1:13;
then U_FT y misses A ` by XBOOLE_0:def_7;
then not y in (A `) ^b by Th8;
hence x in ((A `) ^b) ` by SUBSET_1:29; ::_thesis: verum
end;
hence ((A `) ^b) ` = A ^i by TARSKI:1; ::_thesis: verum
end;
theorem :: FIN_TOPO:18
for FT being non empty RelStr
for A being Subset of FT holds A ^delta = (A ^b) /\ ((A `) ^b)
proof
let FT be non empty RelStr ; ::_thesis: for A being Subset of FT holds A ^delta = (A ^b) /\ ((A `) ^b)
let A be Subset of FT; ::_thesis: A ^delta = (A ^b) /\ ((A `) ^b)
for x being set holds
( x in A ^delta iff x in (A ^b) /\ ((A `) ^b) )
proof
let x be set ; ::_thesis: ( x in A ^delta iff x in (A ^b) /\ ((A `) ^b) )
thus ( x in A ^delta implies x in (A ^b) /\ ((A `) ^b) ) ::_thesis: ( x in (A ^b) /\ ((A `) ^b) implies x in A ^delta )
proof
assume A1: x in A ^delta ; ::_thesis: x in (A ^b) /\ ((A `) ^b)
then reconsider y = x as Element of FT ;
U_FT y meets A ` by A1, Th5;
then A2: x in (A `) ^b ;
U_FT y meets A by A1, Th5;
then x in A ^b ;
hence x in (A ^b) /\ ((A `) ^b) by A2, XBOOLE_0:def_4; ::_thesis: verum
end;
assume A3: x in (A ^b) /\ ((A `) ^b) ; ::_thesis: x in A ^delta
then reconsider y = x as Element of FT ;
x in (A `) ^b by A3, XBOOLE_0:def_4;
then A4: U_FT y meets A ` by Th8;
x in A ^b by A3, XBOOLE_0:def_4;
then U_FT y meets A by Th8;
hence x in A ^delta by A4; ::_thesis: verum
end;
hence A ^delta = (A ^b) /\ ((A `) ^b) by TARSKI:1; ::_thesis: verum
end;
theorem :: FIN_TOPO:19
for FT being non empty RelStr
for A being Subset of FT holds (A `) ^delta = A ^delta
proof
let FT be non empty RelStr ; ::_thesis: for A being Subset of FT holds (A `) ^delta = A ^delta
let A be Subset of FT; ::_thesis: (A `) ^delta = A ^delta
for x being set holds
( x in (A `) ^delta iff x in A ^delta )
proof
let x be set ; ::_thesis: ( x in (A `) ^delta iff x in A ^delta )
thus ( x in (A `) ^delta implies x in A ^delta ) ::_thesis: ( x in A ^delta implies x in (A `) ^delta )
proof
assume A1: x in (A `) ^delta ; ::_thesis: x in A ^delta
then reconsider y = x as Element of FT ;
( U_FT y meets A ` & U_FT y meets (A `) ` ) by A1, Th5;
hence x in A ^delta ; ::_thesis: verum
end;
assume A2: x in A ^delta ; ::_thesis: x in (A `) ^delta
then reconsider y = x as Element of FT ;
( U_FT y meets (A `) ` & U_FT y meets A ` ) by A2, Th5;
hence x in (A `) ^delta ; ::_thesis: verum
end;
hence (A `) ^delta = A ^delta by TARSKI:1; ::_thesis: verum
end;
theorem :: FIN_TOPO:20
for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT st x in A ^s holds
not x in (A \ {x}) ^b
proof
let FT be non empty RelStr ; ::_thesis: for x being Element of FT
for A being Subset of FT st x in A ^s holds
not x in (A \ {x}) ^b
let x be Element of FT; ::_thesis: for A being Subset of FT st x in A ^s holds
not x in (A \ {x}) ^b
let A be Subset of FT; ::_thesis: ( x in A ^s implies not x in (A \ {x}) ^b )
assume x in A ^s ; ::_thesis: not x in (A \ {x}) ^b
then A misses (U_FT x) \ {x} by Th9;
then A /\ ((U_FT x) \ {x}) = {} by XBOOLE_0:def_7;
then A1: (A /\ (U_FT x)) \ {x} = {} by XBOOLE_1:49;
now__::_thesis:_A_\_{x}_misses_U_FT_x
percases ( A /\ (U_FT x) = {} or A /\ (U_FT x) = {x} ) by A1, ZFMISC_1:58;
suppose A /\ (U_FT x) = {} ; ::_thesis: A \ {x} misses U_FT x
then A misses U_FT x by XBOOLE_0:def_7;
hence A \ {x} misses U_FT x by XBOOLE_1:36, XBOOLE_1:63; ::_thesis: verum
end;
suppose A /\ (U_FT x) = {x} ; ::_thesis: A \ {x} misses U_FT x
then ((U_FT x) /\ A) \ {x} = {} by XBOOLE_1:37;
then (U_FT x) /\ (A \ {x}) = {} by XBOOLE_1:49;
hence A \ {x} misses U_FT x by XBOOLE_0:def_7; ::_thesis: verum
end;
end;
end;
hence not x in (A \ {x}) ^b by Th8; ::_thesis: verum
end;
theorem :: FIN_TOPO:21
for FT being non empty RelStr
for A being Subset of FT st A ^s <> {} & card A <> 1 holds
not A is connected
proof
let FT be non empty RelStr ; ::_thesis: for A being Subset of FT st A ^s <> {} & card A <> 1 holds
not A is connected
let A be Subset of FT; ::_thesis: ( A ^s <> {} & card A <> 1 implies not A is connected )
assume that
A1: A ^s <> {} and
A2: card A <> 1 ; ::_thesis: not A is connected
consider z being Element of FT such that
A3: z in A ^s by A1, SUBSET_1:4;
set C = {z};
set B = A \ {z};
( card {z} = 1 & A <> {} ) by A3, Th9, CARD_1:30;
then A4: A \ {z} <> {} by A2, ZFMISC_1:58;
z in A by A3, Th9;
then {z} is Subset of A by SUBSET_1:41;
then A5: A = (A \ {z}) \/ {z} by XBOOLE_1:45;
A6: (U_FT z) \ {z} misses A by A3, Th9;
A7: (A \ {z}) ^b misses {z}
proof
assume (A \ {z}) ^b meets {z} ; ::_thesis: contradiction
then consider x being set such that
A8: x in (A \ {z}) ^b and
A9: x in {z} by XBOOLE_0:3;
reconsider x = x as Element of FT by A8;
A10: x = z by A9, TARSKI:def_1;
U_FT x meets A \ {z} by A8, Th8;
then consider y being set such that
A11: y in U_FT x and
A12: y in A \ {z} by XBOOLE_0:3;
not x in A \ {z} by A9, XBOOLE_0:def_5;
then y in (U_FT x) \ {x} by A11, A12, ZFMISC_1:56;
then (U_FT z) \ {z} meets A \ {z} by A12, A10, XBOOLE_0:3;
then A13: ex w being set st w in ((U_FT z) \ {z}) /\ (A \ {z}) by XBOOLE_0:4;
((U_FT z) \ {z}) /\ (A \ {z}) c= ((U_FT z) \ {z}) /\ A by XBOOLE_1:26, XBOOLE_1:36;
hence contradiction by A6, A13, XBOOLE_0:4; ::_thesis: verum
end;
A \ {z} misses {z} by XBOOLE_1:79;
hence not A is connected by A5, A4, A7, Def16; ::_thesis: verum
end;
theorem :: FIN_TOPO:22
for FT being non empty filled RelStr
for A being Subset of FT holds A ^i c= A
proof
let FT be non empty filled RelStr ; ::_thesis: for A being Subset of FT holds A ^i c= A
let A be Subset of FT; ::_thesis: A ^i c= A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A ^i or x in A )
assume A1: x in A ^i ; ::_thesis: x in A
then reconsider y = x as Element of FT ;
A2: y in U_FT y by Def4;
U_FT y c= A by A1, Th7;
hence x in A by A2; ::_thesis: verum
end;
theorem :: FIN_TOPO:23
for FT being non empty RelStr
for A being Subset of FT st A is open holds
A ` is closed
proof
let FT be non empty RelStr ; ::_thesis: for A being Subset of FT st A is open holds
A ` is closed
let A be Subset of FT; ::_thesis: ( A is open implies A ` is closed )
assume A is open ; ::_thesis: A ` is closed
then A1: A = A ^i by Def14;
A ^i = ((A `) ^b) ` by Th17;
hence A ` is closed by A1, Def15; ::_thesis: verum
end;
theorem :: FIN_TOPO:24
for FT being non empty RelStr
for A being Subset of FT st A is closed holds
A ` is open
proof
let FT be non empty RelStr ; ::_thesis: for A being Subset of FT st A is closed holds
A ` is open
let A be Subset of FT; ::_thesis: ( A is closed implies A ` is open )
assume A is closed ; ::_thesis: A ` is open
then A1: A = A ^b by Def15;
A ^b = ((A `) ^i) ` by Th16;
hence A ` is open by A1, Def14; ::_thesis: verum
end;