:: FINTOPO2 semantic presentation
begin
theorem :: FINTOPO2:1
for FT being non empty RelStr
for A, B being Subset of FT st A c= B holds
A ^i c= B ^i
proof
let FT be non empty RelStr ; ::_thesis: for A, B being Subset of FT st A c= B holds
A ^i c= B ^i
let A, B be Subset of FT; ::_thesis: ( A c= B implies A ^i c= B ^i )
assume A1: A c= B ; ::_thesis: A ^i c= B ^i
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A ^i or x in B ^i )
assume A2: x in A ^i ; ::_thesis: x in B ^i
then reconsider y = x as Element of FT ;
A3: U_FT y c= A by A2, FIN_TOPO:7;
for t being Element of FT st t in U_FT y holds
t in B
proof
let t be Element of FT; ::_thesis: ( t in U_FT y implies t in B )
assume t in U_FT y ; ::_thesis: t in B
then t in A by A3;
hence t in B by A1; ::_thesis: verum
end;
then U_FT y c= B by SUBSET_1:2;
hence x in B ^i ; ::_thesis: verum
end;
theorem Th2: :: FINTOPO2:2
for FT being non empty RelStr
for A being Subset of FT holds A ^delta = (A ^b) /\ ((A ^i) `)
proof
let FT be non empty RelStr ; ::_thesis: for A being Subset of FT holds A ^delta = (A ^b) /\ ((A ^i) `)
let A be Subset of FT; ::_thesis: A ^delta = (A ^b) /\ ((A ^i) `)
for x being set holds
( x in A ^delta iff x in (A ^b) /\ ((A ^i) `) )
proof
let x be set ; ::_thesis: ( x in A ^delta iff x in (A ^b) /\ ((A ^i) `) )
thus ( x in A ^delta implies x in (A ^b) /\ ((A ^i) `) ) ::_thesis: ( x in (A ^b) /\ ((A ^i) `) implies x in A ^delta )
proof
assume A1: x in A ^delta ; ::_thesis: x in (A ^b) /\ ((A ^i) `)
then reconsider y = x as Element of FT ;
U_FT y meets A ` by A1, FIN_TOPO:5;
then y in (((A `) ^b) `) ` ;
then A2: y in (A ^i) ` by FIN_TOPO:17;
U_FT y meets A by A1, FIN_TOPO:5;
then y in A ^b ;
hence x in (A ^b) /\ ((A ^i) `) by A2, XBOOLE_0:def_4; ::_thesis: verum
end;
assume A3: x in (A ^b) /\ ((A ^i) `) ; ::_thesis: x in A ^delta
then reconsider y = x as Element of FT ;
x in (A ^i) ` by A3, XBOOLE_0:def_4;
then x in (((A `) ^b) `) ` by FIN_TOPO:17;
then A4: U_FT y meets A ` by FIN_TOPO:8;
x in A ^b by A3, XBOOLE_0:def_4;
then U_FT y meets A by FIN_TOPO:8;
hence x in A ^delta by A4; ::_thesis: verum
end;
hence A ^delta = (A ^b) /\ ((A ^i) `) by TARSKI:1; ::_thesis: verum
end;
theorem :: FINTOPO2:3
for FT being non empty RelStr
for A being Subset of FT holds A ^delta = (A ^b) \ (A ^i)
proof
let FT be non empty RelStr ; ::_thesis: for A being Subset of FT holds A ^delta = (A ^b) \ (A ^i)
let A be Subset of FT; ::_thesis: A ^delta = (A ^b) \ (A ^i)
for x being set holds
( x in A ^delta iff x in (A ^b) \ (A ^i) )
proof
let x be set ; ::_thesis: ( x in A ^delta iff x in (A ^b) \ (A ^i) )
thus ( x in A ^delta implies x in (A ^b) \ (A ^i) ) ::_thesis: ( x in (A ^b) \ (A ^i) implies x in A ^delta )
proof
assume x in A ^delta ; ::_thesis: x in (A ^b) \ (A ^i)
then x in (A ^b) /\ ((A ^i) `) by Th2;
hence x in (A ^b) \ (A ^i) by SUBSET_1:13; ::_thesis: verum
end;
assume x in (A ^b) \ (A ^i) ; ::_thesis: x in A ^delta
then x in (A ^b) /\ ((A ^i) `) by SUBSET_1:13;
hence x in A ^delta by Th2; ::_thesis: verum
end;
hence A ^delta = (A ^b) \ (A ^i) by TARSKI:1; ::_thesis: verum
end;
theorem :: FINTOPO2:4
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 FIN_TOPO:def_14;
(A `) ^i = (((A `) `) ^b) ` by FIN_TOPO:17
.= (A ^b) ` ;
then A = ((A ^b) `) ` by A1
.= A ^b ;
hence A is closed by FIN_TOPO:def_15; ::_thesis: verum
end;
theorem :: FINTOPO2:5
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 FIN_TOPO:def_15;
(A `) ^b = (((A `) `) ^i) ` by FIN_TOPO:16
.= (A ^i) ` ;
then A = ((A ^i) `) ` by A1
.= A ^i ;
hence A is open by FIN_TOPO:def_14; ::_thesis: verum
end;
definition
let FT be non empty RelStr ;
let x, y be Element of FT;
let A be Subset of FT;
func P_1 (x,y,A) -> Element of BOOLEAN equals :Def1: :: FINTOPO2:def 1
TRUE if ( y in U_FT x & y in A )
otherwise FALSE ;
correctness
coherence
( ( y in U_FT x & y in A implies TRUE is Element of BOOLEAN ) & ( ( not y in U_FT x or not y in A ) implies FALSE is Element of BOOLEAN ) );
consistency
for b1 being Element of BOOLEAN holds verum;
;
end;
:: deftheorem Def1 defines P_1 FINTOPO2:def_1_:_
for FT being non empty RelStr
for x, y being Element of FT
for A being Subset of FT holds
( ( y in U_FT x & y in A implies P_1 (x,y,A) = TRUE ) & ( ( not y in U_FT x or not y in A ) implies P_1 (x,y,A) = FALSE ) );
definition
let FT be non empty RelStr ;
let x, y be Element of FT;
let A be Subset of FT;
func P_2 (x,y,A) -> Element of BOOLEAN equals :Def2: :: FINTOPO2:def 2
TRUE if ( y in U_FT x & y in A ` )
otherwise FALSE ;
correctness
coherence
( ( y in U_FT x & y in A ` implies TRUE is Element of BOOLEAN ) & ( ( not y in U_FT x or not y in A ` ) implies FALSE is Element of BOOLEAN ) );
consistency
for b1 being Element of BOOLEAN holds verum;
;
end;
:: deftheorem Def2 defines P_2 FINTOPO2:def_2_:_
for FT being non empty RelStr
for x, y being Element of FT
for A being Subset of FT holds
( ( y in U_FT x & y in A ` implies P_2 (x,y,A) = TRUE ) & ( ( not y in U_FT x or not y in A ` ) implies P_2 (x,y,A) = FALSE ) );
theorem :: FINTOPO2:6
for FT being non empty RelStr
for x, y being Element of FT
for A being Subset of FT holds
( P_1 (x,y,A) = TRUE iff ( y in U_FT x & y in A ) ) by Def1;
theorem :: FINTOPO2:7
for FT being non empty RelStr
for x, y being Element of FT
for A being Subset of FT holds
( P_2 (x,y,A) = TRUE iff ( y in U_FT x & y in A ` ) ) by Def2;
theorem Th8: :: FINTOPO2:8
for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT holds
( x in A ^delta iff ex y1, y2 being Element of FT st
( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) )
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 ex y1, y2 being Element of FT st
( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) )
let x be Element of FT; ::_thesis: for A being Subset of FT holds
( x in A ^delta iff ex y1, y2 being Element of FT st
( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) )
let A be Subset of FT; ::_thesis: ( x in A ^delta iff ex y1, y2 being Element of FT st
( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) )
A1: ( x in A ^delta implies ex y1, y2 being Element of FT st
( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) )
proof
reconsider z = x as Element of FT ;
assume A2: x in A ^delta ; ::_thesis: ex y1, y2 being Element of FT st
( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE )
then U_FT z meets A by FIN_TOPO:5;
then consider w1 being set such that
A3: w1 in U_FT z and
A4: w1 in A by XBOOLE_0:3;
reconsider w1 = w1 as Element of FT by A3;
take w1 ; ::_thesis: ex y2 being Element of FT st
( P_1 (x,w1,A) = TRUE & P_2 (x,y2,A) = TRUE )
U_FT z meets A ` by A2, FIN_TOPO:5;
then consider w2 being set such that
A5: ( w2 in U_FT z & w2 in A ` ) by XBOOLE_0:3;
take w2 ; ::_thesis: ( w2 is Element of FT & P_1 (x,w1,A) = TRUE & P_2 (x,w2,A) = TRUE )
thus ( w2 is Element of FT & P_1 (x,w1,A) = TRUE & P_2 (x,w2,A) = TRUE ) by A3, A4, A5, Def1, Def2; ::_thesis: verum
end;
( ex y1, y2 being Element of FT st
( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) implies x in A ^delta )
proof
given y1, y2 being Element of FT such that A6: P_1 (x,y1,A) = TRUE and
A7: P_2 (x,y2,A) = TRUE ; ::_thesis: x in A ^delta
( y1 in U_FT x & y1 in A ) by A6, Def1;
then (U_FT x) /\ A <> {} by XBOOLE_0:def_4;
then A8: U_FT x meets A by XBOOLE_0:def_7;
( y2 in U_FT x & y2 in A ` ) by A7, Def2;
then U_FT x meets A ` by XBOOLE_0:3;
hence x in A ^delta by A8; ::_thesis: verum
end;
hence ( x in A ^delta iff ex y1, y2 being Element of FT st
( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) ) by A1; ::_thesis: verum
end;
definition
let FT be non empty RelStr ;
let x, y be Element of FT;
func P_0 (x,y) -> Element of BOOLEAN equals :Def3: :: FINTOPO2:def 3
TRUE if y in U_FT x
otherwise FALSE ;
correctness
coherence
( ( y in U_FT x implies TRUE is Element of BOOLEAN ) & ( not y in U_FT x implies FALSE is Element of BOOLEAN ) );
consistency
for b1 being Element of BOOLEAN holds verum;
;
end;
:: deftheorem Def3 defines P_0 FINTOPO2:def_3_:_
for FT being non empty RelStr
for x, y being Element of FT holds
( ( y in U_FT x implies P_0 (x,y) = TRUE ) & ( not y in U_FT x implies P_0 (x,y) = FALSE ) );
theorem :: FINTOPO2:9
for FT being non empty RelStr
for x, y being Element of FT holds
( P_0 (x,y) = TRUE iff y in U_FT x ) by Def3;
theorem :: FINTOPO2:10
for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT holds
( x in A ^i iff for y being Element of FT st P_0 (x,y) = TRUE holds
P_1 (x,y,A) = TRUE )
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 for y being Element of FT st P_0 (x,y) = TRUE holds
P_1 (x,y,A) = TRUE )
let x be Element of FT; ::_thesis: for A being Subset of FT holds
( x in A ^i iff for y being Element of FT st P_0 (x,y) = TRUE holds
P_1 (x,y,A) = TRUE )
let A be Subset of FT; ::_thesis: ( x in A ^i iff for y being Element of FT st P_0 (x,y) = TRUE holds
P_1 (x,y,A) = TRUE )
A1: ( ( for y being Element of FT st P_0 (x,y) = TRUE holds
P_1 (x,y,A) = TRUE ) implies x in A ^i )
proof
assume A2: for y being Element of FT st P_0 (x,y) = TRUE holds
P_1 (x,y,A) = TRUE ; ::_thesis: x in A ^i
for y being Element of FT st y in U_FT x holds
( y in U_FT x & y in A )
proof
let y be Element of FT; ::_thesis: ( y in U_FT x implies ( y in U_FT x & y in A ) )
assume y in U_FT x ; ::_thesis: ( y in U_FT x & y in A )
then P_0 (x,y) = TRUE by Def3;
then P_1 (x,y,A) = TRUE by A2;
hence ( y in U_FT x & y in A ) by Def1; ::_thesis: verum
end;
then for y being Element of FT st y in U_FT x holds
y in A ;
then U_FT x c= A by SUBSET_1:2;
hence x in A ^i ; ::_thesis: verum
end;
( x in A ^i implies for y being Element of FT st P_0 (x,y) = TRUE holds
P_1 (x,y,A) = TRUE )
proof
assume x in A ^i ; ::_thesis: for y being Element of FT st P_0 (x,y) = TRUE holds
P_1 (x,y,A) = TRUE
then A3: U_FT x c= A by FIN_TOPO:7;
let y be Element of FT; ::_thesis: ( P_0 (x,y) = TRUE implies P_1 (x,y,A) = TRUE )
assume P_0 (x,y) = TRUE ; ::_thesis: P_1 (x,y,A) = TRUE
then y in U_FT x by Def3;
hence P_1 (x,y,A) = TRUE by A3, Def1; ::_thesis: verum
end;
hence ( x in A ^i iff for y being Element of FT st P_0 (x,y) = TRUE holds
P_1 (x,y,A) = TRUE ) by A1; ::_thesis: verum
end;
theorem :: FINTOPO2:11
for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT holds
( x in A ^b iff ex y1 being Element of FT st P_1 (x,y1,A) = TRUE )
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 ex y1 being Element of FT st P_1 (x,y1,A) = TRUE )
let x be Element of FT; ::_thesis: for A being Subset of FT holds
( x in A ^b iff ex y1 being Element of FT st P_1 (x,y1,A) = TRUE )
let A be Subset of FT; ::_thesis: ( x in A ^b iff ex y1 being Element of FT st P_1 (x,y1,A) = TRUE )
A1: ( x in A ^b implies ex y1 being Element of FT st P_1 (x,y1,A) = TRUE )
proof
reconsider z = x as Element of FT ;
assume x in A ^b ; ::_thesis: ex y1 being Element of FT st P_1 (x,y1,A) = TRUE
then U_FT z meets A by FIN_TOPO:8;
then consider w being set such that
A2: w in U_FT z and
A3: w in A by XBOOLE_0:3;
reconsider w = w as Element of FT by A2;
take w ; ::_thesis: P_1 (x,w,A) = TRUE
thus P_1 (x,w,A) = TRUE by A2, A3, Def1; ::_thesis: verum
end;
( ex y1 being Element of FT st P_1 (x,y1,A) = TRUE implies x in A ^b )
proof
given y being Element of FT such that A4: P_1 (x,y,A) = TRUE ; ::_thesis: x in A ^b
( y in U_FT x & y in A ) by A4, Def1;
then y in (U_FT x) /\ A by XBOOLE_0:def_4;
then U_FT x meets A by XBOOLE_0:def_7;
hence x in A ^b ; ::_thesis: verum
end;
hence ( x in A ^b iff ex y1 being Element of FT st P_1 (x,y1,A) = TRUE ) by A1; ::_thesis: verum
end;
definition
let FT be non empty RelStr ;
let x be Element of FT;
let A be Subset of FT;
func P_A (x,A) -> Element of BOOLEAN equals :Def4: :: FINTOPO2:def 4
TRUE if x in A
otherwise FALSE ;
correctness
coherence
( ( x in A implies TRUE is Element of BOOLEAN ) & ( not x in A implies FALSE is Element of BOOLEAN ) );
consistency
for b1 being Element of BOOLEAN holds verum;
;
end;
:: deftheorem Def4 defines P_A FINTOPO2:def_4_:_
for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT holds
( ( x in A implies P_A (x,A) = TRUE ) & ( not x in A implies P_A (x,A) = FALSE ) );
theorem :: FINTOPO2:12
for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT holds
( P_A (x,A) = TRUE iff x in A ) by Def4;
theorem :: FINTOPO2:13
for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT holds
( x in A ^deltai iff ( ex y1, y2 being Element of FT st
( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = TRUE ) )
proof
let FT be non empty RelStr ; ::_thesis: for x being Element of FT
for A being Subset of FT holds
( x in A ^deltai iff ( ex y1, y2 being Element of FT st
( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = TRUE ) )
let x be Element of FT; ::_thesis: for A being Subset of FT holds
( x in A ^deltai iff ( ex y1, y2 being Element of FT st
( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = TRUE ) )
let A be Subset of FT; ::_thesis: ( x in A ^deltai iff ( ex y1, y2 being Element of FT st
( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = TRUE ) )
A1: ( ex y1, y2 being Element of FT st
( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = TRUE implies x in A ^deltai )
proof
assume ( ex y1, y2 being Element of FT st
( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = TRUE ) ; ::_thesis: x in A ^deltai
then ( x in A ^delta & x in A ) by Def4, Th8;
hence x in A ^deltai by XBOOLE_0:def_4; ::_thesis: verum
end;
( x in A ^deltai implies ( ex y1, y2 being Element of FT st
( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = TRUE ) )
proof
assume x in A ^deltai ; ::_thesis: ( ex y1, y2 being Element of FT st
( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = TRUE )
then ( x in A & x in A ^delta ) by XBOOLE_0:def_4;
hence ( ex y1, y2 being Element of FT st
( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = TRUE ) by Def4, Th8; ::_thesis: verum
end;
hence ( x in A ^deltai iff ( ex y1, y2 being Element of FT st
( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = TRUE ) ) by A1; ::_thesis: verum
end;
theorem :: FINTOPO2:14
for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT holds
( x in A ^deltao iff ( ex y1, y2 being Element of FT st
( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = FALSE ) )
proof
let FT be non empty RelStr ; ::_thesis: for x being Element of FT
for A being Subset of FT holds
( x in A ^deltao iff ( ex y1, y2 being Element of FT st
( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = FALSE ) )
let x be Element of FT; ::_thesis: for A being Subset of FT holds
( x in A ^deltao iff ( ex y1, y2 being Element of FT st
( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = FALSE ) )
let A be Subset of FT; ::_thesis: ( x in A ^deltao iff ( ex y1, y2 being Element of FT st
( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = FALSE ) )
A1: ( ex y1, y2 being Element of FT st
( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = FALSE implies x in A ^deltao )
proof
assume that
A2: ex y1, y2 being Element of FT st
( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) and
A3: P_A (x,A) = FALSE ; ::_thesis: x in A ^deltao
not x in A by A3, Def4;
then A4: x in A ` by XBOOLE_0:def_5;
x in A ^delta by A2, Th8;
hence x in A ^deltao by A4, XBOOLE_0:def_4; ::_thesis: verum
end;
( x in A ^deltao implies ( ex y1, y2 being Element of FT st
( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = FALSE ) )
proof
assume A5: x in A ^deltao ; ::_thesis: ( ex y1, y2 being Element of FT st
( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = FALSE )
then x in A ` by XBOOLE_0:def_4;
then A6: not x in A by XBOOLE_0:def_5;
x in A ^delta by A5, XBOOLE_0:def_4;
hence ( ex y1, y2 being Element of FT st
( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = FALSE ) by A6, Def4, Th8; ::_thesis: verum
end;
hence ( x in A ^deltao iff ( ex y1, y2 being Element of FT st
( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = FALSE ) ) by A1; ::_thesis: verum
end;
definition
let FT be non empty RelStr ;
let x, y be Element of FT;
func P_e (x,y) -> Element of BOOLEAN equals :Def5: :: FINTOPO2:def 5
TRUE if x = y
otherwise FALSE ;
correctness
coherence
( ( x = y implies TRUE is Element of BOOLEAN ) & ( not x = y implies FALSE is Element of BOOLEAN ) );
consistency
for b1 being Element of BOOLEAN holds verum;
;
end;
:: deftheorem Def5 defines P_e FINTOPO2:def_5_:_
for FT being non empty RelStr
for x, y being Element of FT holds
( ( x = y implies P_e (x,y) = TRUE ) & ( not x = y implies P_e (x,y) = FALSE ) );
theorem :: FINTOPO2:15
for FT being non empty RelStr
for x, y being Element of FT holds
( P_e (x,y) = TRUE iff x = y ) by Def5;
theorem :: FINTOPO2:16
for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT holds
( x in A ^s iff ( P_A (x,A) = TRUE & ( for y being Element of FT holds
( not P_1 (x,y,A) = TRUE or not P_e (x,y) = FALSE ) ) ) )
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 ( P_A (x,A) = TRUE & ( for y being Element of FT holds
( not P_1 (x,y,A) = TRUE or not P_e (x,y) = FALSE ) ) ) )
let x be Element of FT; ::_thesis: for A being Subset of FT holds
( x in A ^s iff ( P_A (x,A) = TRUE & ( for y being Element of FT holds
( not P_1 (x,y,A) = TRUE or not P_e (x,y) = FALSE ) ) ) )
let A be Subset of FT; ::_thesis: ( x in A ^s iff ( P_A (x,A) = TRUE & ( for y being Element of FT holds
( not P_1 (x,y,A) = TRUE or not P_e (x,y) = FALSE ) ) ) )
A1: ( x in A ^s implies ( P_A (x,A) = TRUE & ( for y being Element of FT holds
( not P_1 (x,y,A) = TRUE or not P_e (x,y) = FALSE ) ) ) )
proof
assume A2: x in A ^s ; ::_thesis: ( P_A (x,A) = TRUE & ( for y being Element of FT holds
( not P_1 (x,y,A) = TRUE or not P_e (x,y) = FALSE ) ) )
then (U_FT x) \ {x} misses A by FIN_TOPO:9;
then A3: ((U_FT x) \ {x}) /\ A = {} by XBOOLE_0:def_7;
A4: for y being Element of FT holds
( not P_1 (x,y,A) = TRUE or not P_e (x,y) = FALSE )
proof
given y being Element of FT such that A5: P_1 (x,y,A) = TRUE and
A6: P_e (x,y) = FALSE ; ::_thesis: contradiction
not x = y by A6, Def5;
then A7: not y in {x} by TARSKI:def_1;
y in U_FT x by A5, Def1;
then A8: y in (U_FT x) \ {x} by A7, XBOOLE_0:def_5;
y in A by A5, Def1;
hence contradiction by A3, A8, XBOOLE_0:def_4; ::_thesis: verum
end;
x in A by A2, FIN_TOPO:9;
hence ( P_A (x,A) = TRUE & ( for y being Element of FT holds
( not P_1 (x,y,A) = TRUE or not P_e (x,y) = FALSE ) ) ) by A4, Def4; ::_thesis: verum
end;
( P_A (x,A) = TRUE & ( for y being Element of FT holds
( not P_1 (x,y,A) = TRUE or not P_e (x,y) = FALSE ) ) implies x in A ^s )
proof
assume that
A9: P_A (x,A) = TRUE and
A10: for y being Element of FT holds
( not P_1 (x,y,A) = TRUE or not P_e (x,y) = FALSE ) ; ::_thesis: x in A ^s
for y being Element of FT holds not y in ((U_FT x) \ {x}) /\ A
proof
let y be Element of FT; ::_thesis: not y in ((U_FT x) \ {x}) /\ A
( not P_1 (x,y,A) = TRUE or not P_e (x,y) = FALSE ) by A10;
then ( not y in U_FT x or x = y or not y in A ) by Def1, Def5;
then ( not y in U_FT x or y in {x} or not y in A ) by TARSKI:def_1;
then ( not y in (U_FT x) \ {x} or not y in A ) by XBOOLE_0:def_5;
hence not y in ((U_FT x) \ {x}) /\ A by XBOOLE_0:def_4; ::_thesis: verum
end;
then ((U_FT x) \ {x}) /\ A = {} by SUBSET_1:4;
then A11: (U_FT x) \ {x} misses A by XBOOLE_0:def_7;
x in A by A9, Def4;
hence x in A ^s by A11; ::_thesis: verum
end;
hence ( x in A ^s iff ( P_A (x,A) = TRUE & ( for y being Element of FT holds
( not P_1 (x,y,A) = TRUE or not P_e (x,y) = FALSE ) ) ) ) by A1; ::_thesis: verum
end;
theorem :: FINTOPO2:17
for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT holds
( x in A ^n iff ( P_A (x,A) = TRUE & ex y being Element of FT st
( P_1 (x,y,A) = TRUE & P_e (x,y) = FALSE ) ) )
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 ( P_A (x,A) = TRUE & ex y being Element of FT st
( P_1 (x,y,A) = TRUE & P_e (x,y) = FALSE ) ) )
let x be Element of FT; ::_thesis: for A being Subset of FT holds
( x in A ^n iff ( P_A (x,A) = TRUE & ex y being Element of FT st
( P_1 (x,y,A) = TRUE & P_e (x,y) = FALSE ) ) )
let A be Subset of FT; ::_thesis: ( x in A ^n iff ( P_A (x,A) = TRUE & ex y being Element of FT st
( P_1 (x,y,A) = TRUE & P_e (x,y) = FALSE ) ) )
A1: ( x in A ^n implies ( P_A (x,A) = TRUE & ex y being Element of FT st
( P_1 (x,y,A) = TRUE & P_e (x,y) = FALSE ) ) )
proof
assume A2: x in A ^n ; ::_thesis: ( P_A (x,A) = TRUE & ex y being Element of FT st
( P_1 (x,y,A) = TRUE & P_e (x,y) = FALSE ) )
then (U_FT x) \ {x} meets A by FIN_TOPO:10;
then ((U_FT x) \ {x}) /\ A <> {} by XBOOLE_0:def_7;
then consider y being Element of FT such that
A3: y in ((U_FT x) \ {x}) /\ A by SUBSET_1:4;
A4: y in (U_FT x) \ {x} by A3, XBOOLE_0:def_4;
then A5: y in U_FT x by XBOOLE_0:def_5;
not y in {x} by A4, XBOOLE_0:def_5;
then not x = y by TARSKI:def_1;
then A6: P_e (x,y) = FALSE by Def5;
y in A by A3, XBOOLE_0:def_4;
then A7: P_1 (x,y,A) = TRUE by A5, Def1;
x in A by A2, FIN_TOPO:10;
hence ( P_A (x,A) = TRUE & ex y being Element of FT st
( P_1 (x,y,A) = TRUE & P_e (x,y) = FALSE ) ) by A6, A7, Def4; ::_thesis: verum
end;
( P_A (x,A) = TRUE & ex y being Element of FT st
( P_1 (x,y,A) = TRUE & P_e (x,y) = FALSE ) implies x in A ^n )
proof
assume that
A8: P_A (x,A) = TRUE and
A9: ex y being Element of FT st
( P_1 (x,y,A) = TRUE & P_e (x,y) = FALSE ) ; ::_thesis: x in A ^n
consider y being Element of FT such that
A10: P_1 (x,y,A) = TRUE and
A11: P_e (x,y) = FALSE by A9;
x <> y by A11, Def5;
then A12: not y in {x} by TARSKI:def_1;
y in U_FT x by A10, Def1;
then A13: y in (U_FT x) \ {x} by A12, XBOOLE_0:def_5;
y in A by A10, Def1;
then A14: (U_FT x) \ {x} meets A by A13, XBOOLE_0:3;
x in A by A8, Def4;
hence x in A ^n by A14, FIN_TOPO:10; ::_thesis: verum
end;
hence ( x in A ^n iff ( P_A (x,A) = TRUE & ex y being Element of FT st
( P_1 (x,y,A) = TRUE & P_e (x,y) = FALSE ) ) ) by A1; ::_thesis: verum
end;
theorem :: FINTOPO2:18
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
( P_A (y,A) = TRUE & P_0 (y,x) = TRUE ) )
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
( P_A (y,A) = TRUE & P_0 (y,x) = TRUE ) )
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
( P_A (y,A) = TRUE & P_0 (y,x) = TRUE ) )
let A be Subset of FT; ::_thesis: ( x in A ^f iff ex y being Element of FT st
( P_A (y,A) = TRUE & P_0 (y,x) = TRUE ) )
A1: ( ex y being Element of FT st
( P_A (y,A) = TRUE & P_0 (y,x) = TRUE ) implies x in A ^f )
proof
assume ex y being Element of FT st
( P_A (y,A) = TRUE & P_0 (y,x) = TRUE ) ; ::_thesis: x in A ^f
then consider y being Element of FT such that
A2: ( P_A (y,A) = TRUE & P_0 (y,x) = TRUE ) ;
( y in A & x in U_FT y ) by A2, Def3, Def4;
hence x in A ^f ; ::_thesis: verum
end;
( x in A ^f implies ex y being Element of FT st
( P_A (y,A) = TRUE & P_0 (y,x) = TRUE ) )
proof
assume x in A ^f ; ::_thesis: ex y being Element of FT st
( P_A (y,A) = TRUE & P_0 (y,x) = TRUE )
then consider y being Element of FT such that
A3: ( y in A & x in U_FT y ) by FIN_TOPO:11;
( P_A (y,A) = TRUE & P_0 (y,x) = TRUE ) by A3, Def3, Def4;
hence ex y being Element of FT st
( P_A (y,A) = TRUE & P_0 (y,x) = TRUE ) ; ::_thesis: verum
end;
hence ( x in A ^f iff ex y being Element of FT st
( P_A (y,A) = TRUE & P_0 (y,x) = TRUE ) ) by A1; ::_thesis: verum
end;
begin
definition
attrc1 is strict ;
struct FMT_Space_Str -> 1-sorted ;
aggrFMT_Space_Str(# carrier, BNbd #) -> FMT_Space_Str ;
sel BNbd c1 -> Function of the carrier of c1,(bool (bool the carrier of c1));
end;
registration
cluster non empty strict for FMT_Space_Str ;
existence
ex b1 being FMT_Space_Str st
( not b1 is empty & b1 is strict )
proof
set D = the non empty set ;
set f = the Function of the non empty set ,(bool (bool the non empty set ));
take FMT_Space_Str(# the non empty set , the Function of the non empty set ,(bool (bool the non empty set )) #) ; ::_thesis: ( not FMT_Space_Str(# the non empty set , the Function of the non empty set ,(bool (bool the non empty set )) #) is empty & FMT_Space_Str(# the non empty set , the Function of the non empty set ,(bool (bool the non empty set )) #) is strict )
thus not the carrier of FMT_Space_Str(# the non empty set , the Function of the non empty set ,(bool (bool the non empty set )) #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: FMT_Space_Str(# the non empty set , the Function of the non empty set ,(bool (bool the non empty set )) #) is strict
thus FMT_Space_Str(# the non empty set , the Function of the non empty set ,(bool (bool the non empty set )) #) is strict ; ::_thesis: verum
end;
end;
definition
let FMT be non empty FMT_Space_Str ;
let x be Element of FMT;
func U_FMT x -> Subset-Family of FMT equals :: FINTOPO2:def 6
the BNbd of FMT . x;
correctness
coherence
the BNbd of FMT . x is Subset-Family of FMT;
;
end;
:: deftheorem defines U_FMT FINTOPO2:def_6_:_
for FMT being non empty FMT_Space_Str
for x being Element of FMT holds U_FMT x = the BNbd of FMT . x;
definition
let T be non empty TopStruct ;
func NeighSp T -> non empty strict FMT_Space_Str means :: FINTOPO2:def 7
( the carrier of it = the carrier of T & ( for x being Point of it holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) );
existence
ex b1 being non empty strict FMT_Space_Str st
( the carrier of b1 = the carrier of T & ( for x being Point of b1 holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) )
proof
ex IT being non empty strict FMT_Space_Str st
( the carrier of IT = the carrier of T & ( for x being Point of IT holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) )
proof
deffunc H1( set ) -> set = { V where V is Subset of T : ( V in the topology of T & $1 in V ) } ;
A1: for x being Element of T holds H1(x) in bool (bool the carrier of T)
proof
let x be Element of T; ::_thesis: H1(x) in bool (bool the carrier of T)
now__::_thesis:_for_Y_being_set_st_Y_in__{__V_where_V_is_Subset_of_T_:_(_V_in_the_topology_of_T_&_x_in_V_)__}__holds_
Y_in_bool_the_carrier_of_T
let Y be set ; ::_thesis: ( Y in { V where V is Subset of T : ( V in the topology of T & x in V ) } implies Y in bool the carrier of T )
assume Y in { V where V is Subset of T : ( V in the topology of T & x in V ) } ; ::_thesis: Y in bool the carrier of T
then ex V being Subset of T st
( V = Y & V in the topology of T & x in V ) ;
hence Y in bool the carrier of T ; ::_thesis: verum
end;
then { V where V is Subset of T : ( V in the topology of T & x in V ) } c= bool the carrier of T by TARSKI:def_3;
hence H1(x) in bool (bool the carrier of T) ; ::_thesis: verum
end;
consider f being Function of the carrier of T,(bool (bool the carrier of T)) such that
A2: for x being Element of T holds f . x = H1(x) from FUNCT_2:sch_8(A1);
reconsider IT = FMT_Space_Str(# the carrier of T,f #) as non empty strict FMT_Space_Str ;
take IT ; ::_thesis: ( the carrier of IT = the carrier of T & ( for x being Point of IT holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) )
thus ( the carrier of IT = the carrier of T & ( for x being Point of IT holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) ) by A2; ::_thesis: verum
end;
hence ex b1 being non empty strict FMT_Space_Str st
( the carrier of b1 = the carrier of T & ( for x being Point of b1 holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being non empty strict FMT_Space_Str st the carrier of b1 = the carrier of T & ( for x being Point of b1 holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) & the carrier of b2 = the carrier of T & ( for x being Point of b2 holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) holds
b1 = b2
proof
let it1, it2 be non empty strict FMT_Space_Str ; ::_thesis: ( the carrier of it1 = the carrier of T & ( for x being Point of it1 holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) & the carrier of it2 = the carrier of T & ( for x being Point of it2 holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) implies it1 = it2 )
assume that
A3: the carrier of it1 = the carrier of T and
A4: for x being Point of it1 holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } and
A5: the carrier of it2 = the carrier of T and
A6: for x being Point of it2 holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ; ::_thesis: it1 = it2
A7: for x being Element of it2 holds the BNbd of it2 . x = { V where V is Subset of T : ( V in the topology of T & x in V ) }
proof
let x be Element of it2; ::_thesis: the BNbd of it2 . x = { V where V is Subset of T : ( V in the topology of T & x in V ) }
the BNbd of it2 . x = U_FMT x ;
hence the BNbd of it2 . x = { V where V is Subset of T : ( V in the topology of T & x in V ) } by A6; ::_thesis: verum
end;
A8: for x being Element of it1 holds the BNbd of it1 . x = { V where V is Subset of T : ( V in the topology of T & x in V ) }
proof
let x be Element of it1; ::_thesis: the BNbd of it1 . x = { V where V is Subset of T : ( V in the topology of T & x in V ) }
the BNbd of it1 . x = U_FMT x ;
hence the BNbd of it1 . x = { V where V is Subset of T : ( V in the topology of T & x in V ) } by A4; ::_thesis: verum
end;
now__::_thesis:_for_x_being_Point_of_it1_holds_the_BNbd_of_it1_._x_=_the_BNbd_of_it2_._x
let x be Point of it1; ::_thesis: the BNbd of it1 . x = the BNbd of it2 . x
thus the BNbd of it1 . x = { V where V is Subset of T : ( V in the topology of T & x in V ) } by A8
.= the BNbd of it2 . x by A3, A5, A7 ; ::_thesis: verum
end;
hence it1 = it2 by A3, A5, FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem defines NeighSp FINTOPO2:def_7_:_
for T being non empty TopStruct
for b2 being non empty strict FMT_Space_Str holds
( b2 = NeighSp T iff ( the carrier of b2 = the carrier of T & ( for x being Point of b2 holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) ) );
definition
let IT be non empty FMT_Space_Str ;
attrIT is Fo_filled means :Def8: :: FINTOPO2:def 8
for x being Element of IT
for D being Subset of IT st D in U_FMT x holds
x in D;
end;
:: deftheorem Def8 defines Fo_filled FINTOPO2:def_8_:_
for IT being non empty FMT_Space_Str holds
( IT is Fo_filled iff for x being Element of IT
for D being Subset of IT st D in U_FMT x holds
x in D );
definition
let FMT be non empty FMT_Space_Str ;
let A be Subset of FMT;
funcA ^Fodelta -> Subset of FMT equals :: FINTOPO2:def 9
{ x where x is Element of FMT : for W being Subset of FMT st W in U_FMT x holds
( W meets A & W meets A ` ) } ;
coherence
{ x where x is Element of FMT : for W being Subset of FMT st W in U_FMT x holds
( W meets A & W meets A ` ) } is Subset of FMT
proof
defpred S1[ Element of FMT] means for W being Subset of FMT st W in U_FMT $1 holds
( W meets A & W meets A ` );
{ x where x is Element of FMT : S1[x] } is Subset of FMT from DOMAIN_1:sch_7();
hence { x where x is Element of FMT : for W being Subset of FMT st W in U_FMT x holds
( W meets A & W meets A ` ) } is Subset of FMT ; ::_thesis: verum
end;
end;
:: deftheorem defines ^Fodelta FINTOPO2:def_9_:_
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Fodelta = { x where x is Element of FMT : for W being Subset of FMT st W in U_FMT x holds
( W meets A & W meets A ` ) } ;
theorem Th19: :: FINTOPO2:19
for FMT being non empty FMT_Space_Str
for x being Element of FMT
for A being Subset of FMT holds
( x in A ^Fodelta iff for W being Subset of FMT st W in U_FMT x holds
( W meets A & W meets A ` ) )
proof
let FMT be non empty FMT_Space_Str ; ::_thesis: for x being Element of FMT
for A being Subset of FMT holds
( x in A ^Fodelta iff for W being Subset of FMT st W in U_FMT x holds
( W meets A & W meets A ` ) )
let x be Element of FMT; ::_thesis: for A being Subset of FMT holds
( x in A ^Fodelta iff for W being Subset of FMT st W in U_FMT x holds
( W meets A & W meets A ` ) )
let A be Subset of FMT; ::_thesis: ( x in A ^Fodelta iff for W being Subset of FMT st W in U_FMT x holds
( W meets A & W meets A ` ) )
thus ( x in A ^Fodelta implies for W being Subset of FMT st W in U_FMT x holds
( W meets A & W meets A ` ) ) ::_thesis: ( ( for W being Subset of FMT st W in U_FMT x holds
( W meets A & W meets A ` ) ) implies x in A ^Fodelta )
proof
assume x in A ^Fodelta ; ::_thesis: for W being Subset of FMT st W in U_FMT x holds
( W meets A & W meets A ` )
then ex y being Element of FMT st
( y = x & ( for W being Subset of FMT st W in U_FMT y holds
( W meets A & W meets A ` ) ) ) ;
hence for W being Subset of FMT st W in U_FMT x holds
( W meets A & W meets A ` ) ; ::_thesis: verum
end;
assume for W being Subset of FMT st W in U_FMT x holds
( W meets A & W meets A ` ) ; ::_thesis: x in A ^Fodelta
hence x in A ^Fodelta ; ::_thesis: verum
end;
definition
let FMT be non empty FMT_Space_Str ;
let A be Subset of FMT;
funcA ^Fob -> Subset of FMT equals :: FINTOPO2:def 10
{ x where x is Element of FMT : for W being Subset of FMT st W in U_FMT x holds
W meets A } ;
coherence
{ x where x is Element of FMT : for W being Subset of FMT st W in U_FMT x holds
W meets A } is Subset of FMT
proof
defpred S1[ Element of FMT] means for W being Subset of FMT st W in U_FMT $1 holds
W meets A;
{ x where x is Element of FMT : S1[x] } is Subset of FMT from DOMAIN_1:sch_7();
hence { x where x is Element of FMT : for W being Subset of FMT st W in U_FMT x holds
W meets A } is Subset of FMT ; ::_thesis: verum
end;
end;
:: deftheorem defines ^Fob FINTOPO2:def_10_:_
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Fob = { x where x is Element of FMT : for W being Subset of FMT st W in U_FMT x holds
W meets A } ;
theorem Th20: :: FINTOPO2:20
for FMT being non empty FMT_Space_Str
for x being Element of FMT
for A being Subset of FMT holds
( x in A ^Fob iff for W being Subset of FMT st W in U_FMT x holds
W meets A )
proof
let FMT be non empty FMT_Space_Str ; ::_thesis: for x being Element of FMT
for A being Subset of FMT holds
( x in A ^Fob iff for W being Subset of FMT st W in U_FMT x holds
W meets A )
let x be Element of FMT; ::_thesis: for A being Subset of FMT holds
( x in A ^Fob iff for W being Subset of FMT st W in U_FMT x holds
W meets A )
let A be Subset of FMT; ::_thesis: ( x in A ^Fob iff for W being Subset of FMT st W in U_FMT x holds
W meets A )
thus ( x in A ^Fob implies for W being Subset of FMT st W in U_FMT x holds
W meets A ) ::_thesis: ( ( for W being Subset of FMT st W in U_FMT x holds
W meets A ) implies x in A ^Fob )
proof
assume x in A ^Fob ; ::_thesis: for W being Subset of FMT st W in U_FMT x holds
W meets A
then ex y being Element of FMT st
( y = x & ( for W being Subset of FMT st W in U_FMT y holds
W meets A ) ) ;
hence for W being Subset of FMT st W in U_FMT x holds
W meets A ; ::_thesis: verum
end;
assume for W being Subset of FMT st W in U_FMT x holds
W meets A ; ::_thesis: x in A ^Fob
hence x in A ^Fob ; ::_thesis: verum
end;
definition
let FMT be non empty FMT_Space_Str ;
let A be Subset of FMT;
funcA ^Foi -> Subset of FMT equals :: FINTOPO2:def 11
{ x where x is Element of FMT : ex V being Subset of FMT st
( V in U_FMT x & V c= A ) } ;
coherence
{ x where x is Element of FMT : ex V being Subset of FMT st
( V in U_FMT x & V c= A ) } is Subset of FMT
proof
defpred S1[ Element of FMT] means ex V being Subset of FMT st
( V in U_FMT $1 & V c= A );
{ x where x is Element of FMT : S1[x] } is Subset of FMT from DOMAIN_1:sch_7();
hence { x where x is Element of FMT : ex V being Subset of FMT st
( V in U_FMT x & V c= A ) } is Subset of FMT ; ::_thesis: verum
end;
end;
:: deftheorem defines ^Foi FINTOPO2:def_11_:_
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Foi = { x where x is Element of FMT : ex V being Subset of FMT st
( V in U_FMT x & V c= A ) } ;
theorem Th21: :: FINTOPO2:21
for FMT being non empty FMT_Space_Str
for x being Element of FMT
for A being Subset of FMT holds
( x in A ^Foi iff ex V being Subset of FMT st
( V in U_FMT x & V c= A ) )
proof
let FMT be non empty FMT_Space_Str ; ::_thesis: for x being Element of FMT
for A being Subset of FMT holds
( x in A ^Foi iff ex V being Subset of FMT st
( V in U_FMT x & V c= A ) )
let x be Element of FMT; ::_thesis: for A being Subset of FMT holds
( x in A ^Foi iff ex V being Subset of FMT st
( V in U_FMT x & V c= A ) )
let A be Subset of FMT; ::_thesis: ( x in A ^Foi iff ex V being Subset of FMT st
( V in U_FMT x & V c= A ) )
thus ( x in A ^Foi implies ex V being Subset of FMT st
( V in U_FMT x & V c= A ) ) ::_thesis: ( ex V being Subset of FMT st
( V in U_FMT x & V c= A ) implies x in A ^Foi )
proof
assume x in A ^Foi ; ::_thesis: ex V being Subset of FMT st
( V in U_FMT x & V c= A )
then ex y being Element of FMT st
( y = x & ex V being Subset of FMT st
( V in U_FMT y & V c= A ) ) ;
hence ex V being Subset of FMT st
( V in U_FMT x & V c= A ) ; ::_thesis: verum
end;
assume ex V being Subset of FMT st
( V in U_FMT x & V c= A ) ; ::_thesis: x in A ^Foi
hence x in A ^Foi ; ::_thesis: verum
end;
definition
let FMT be non empty FMT_Space_Str ;
let A be Subset of FMT;
funcA ^Fos -> Subset of FMT equals :: FINTOPO2:def 12
{ x where x is Element of FMT : ( x in A & ex V being Subset of FMT st
( V in U_FMT x & V \ {x} misses A ) ) } ;
coherence
{ x where x is Element of FMT : ( x in A & ex V being Subset of FMT st
( V in U_FMT x & V \ {x} misses A ) ) } is Subset of FMT
proof
defpred S1[ Element of FMT] means ( $1 in A & ex V being Subset of FMT st
( V in U_FMT $1 & V \ {$1} misses A ) );
{ x where x is Element of FMT : S1[x] } is Subset of FMT from DOMAIN_1:sch_7();
hence { x where x is Element of FMT : ( x in A & ex V being Subset of FMT st
( V in U_FMT x & V \ {x} misses A ) ) } is Subset of FMT ; ::_thesis: verum
end;
end;
:: deftheorem defines ^Fos FINTOPO2:def_12_:_
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Fos = { x where x is Element of FMT : ( x in A & ex V being Subset of FMT st
( V in U_FMT x & V \ {x} misses A ) ) } ;
theorem Th22: :: FINTOPO2:22
for FMT being non empty FMT_Space_Str
for x being Element of FMT
for A being Subset of FMT holds
( x in A ^Fos iff ( x in A & ex V being Subset of FMT st
( V in U_FMT x & V \ {x} misses A ) ) )
proof
let FMT be non empty FMT_Space_Str ; ::_thesis: for x being Element of FMT
for A being Subset of FMT holds
( x in A ^Fos iff ( x in A & ex V being Subset of FMT st
( V in U_FMT x & V \ {x} misses A ) ) )
let x be Element of FMT; ::_thesis: for A being Subset of FMT holds
( x in A ^Fos iff ( x in A & ex V being Subset of FMT st
( V in U_FMT x & V \ {x} misses A ) ) )
let A be Subset of FMT; ::_thesis: ( x in A ^Fos iff ( x in A & ex V being Subset of FMT st
( V in U_FMT x & V \ {x} misses A ) ) )
thus ( x in A ^Fos implies ( x in A & ex V being Subset of FMT st
( V in U_FMT x & V \ {x} misses A ) ) ) ::_thesis: ( x in A & ex V being Subset of FMT st
( V in U_FMT x & V \ {x} misses A ) implies x in A ^Fos )
proof
assume x in A ^Fos ; ::_thesis: ( x in A & ex V being Subset of FMT st
( V in U_FMT x & V \ {x} misses A ) )
then ex y being Element of FMT st
( y = x & y in A & ex V being Subset of FMT st
( V in U_FMT y & V \ {y} misses A ) ) ;
hence ( x in A & ex V being Subset of FMT st
( V in U_FMT x & V \ {x} misses A ) ) ; ::_thesis: verum
end;
assume ( x in A & ex V being Subset of FMT st
( V in U_FMT x & V \ {x} misses A ) ) ; ::_thesis: x in A ^Fos
hence x in A ^Fos ; ::_thesis: verum
end;
definition
let FMT be non empty FMT_Space_Str ;
let A be Subset of FMT;
funcA ^Fon -> Subset of FMT equals :: FINTOPO2:def 13
A \ (A ^Fos);
coherence
A \ (A ^Fos) is Subset of FMT ;
end;
:: deftheorem defines ^Fon FINTOPO2:def_13_:_
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Fon = A \ (A ^Fos);
theorem :: FINTOPO2:23
for FMT being non empty FMT_Space_Str
for x being Element of FMT
for A being Subset of FMT holds
( x in A ^Fon iff ( x in A & ( for V being Subset of FMT st V in U_FMT x holds
V \ {x} meets A ) ) )
proof
let FMT be non empty FMT_Space_Str ; ::_thesis: for x being Element of FMT
for A being Subset of FMT holds
( x in A ^Fon iff ( x in A & ( for V being Subset of FMT st V in U_FMT x holds
V \ {x} meets A ) ) )
let x be Element of FMT; ::_thesis: for A being Subset of FMT holds
( x in A ^Fon iff ( x in A & ( for V being Subset of FMT st V in U_FMT x holds
V \ {x} meets A ) ) )
let A be Subset of FMT; ::_thesis: ( x in A ^Fon iff ( x in A & ( for V being Subset of FMT st V in U_FMT x holds
V \ {x} meets A ) ) )
thus ( x in A ^Fon implies ( x in A & ( for V being Subset of FMT st V in U_FMT x holds
V \ {x} meets A ) ) ) ::_thesis: ( x in A & ( for V being Subset of FMT st V in U_FMT x holds
V \ {x} meets A ) implies x in A ^Fon )
proof
assume x in A ^Fon ; ::_thesis: ( x in A & ( for V being Subset of FMT st V in U_FMT x holds
V \ {x} meets A ) )
then ( x in A & not x in A ^Fos ) by XBOOLE_0:def_5;
hence ( x in A & ( for V being Subset of FMT st V in U_FMT x holds
V \ {x} meets A ) ) ; ::_thesis: verum
end;
assume that
A1: x in A and
A2: for V being Subset of FMT st V in U_FMT x holds
V \ {x} meets A ; ::_thesis: x in A ^Fon
not x in A ^Fos by A2, Th22;
hence x in A ^Fon by A1, XBOOLE_0:def_5; ::_thesis: verum
end;
theorem Th24: :: FINTOPO2:24
for FMT being non empty FMT_Space_Str
for A, B being Subset of FMT st A c= B holds
A ^Fob c= B ^Fob
proof
let FMT be non empty FMT_Space_Str ; ::_thesis: for A, B being Subset of FMT st A c= B holds
A ^Fob c= B ^Fob
let A, B be Subset of FMT; ::_thesis: ( A c= B implies A ^Fob c= B ^Fob )
assume A1: A c= B ; ::_thesis: A ^Fob c= B ^Fob
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A ^Fob or x in B ^Fob )
assume A2: x in A ^Fob ; ::_thesis: x in B ^Fob
then reconsider y = x as Element of FMT ;
for W being Subset of FMT st W in U_FMT y holds
W meets B
proof
let W be Subset of FMT; ::_thesis: ( W in U_FMT y implies W meets B )
assume W in U_FMT y ; ::_thesis: W meets B
then W meets A by A2, Th20;
then ex z being set st
( z in W & z in A ) by XBOOLE_0:3;
hence W /\ B <> {} by A1, XBOOLE_0:def_4; :: according to XBOOLE_0:def_7 ::_thesis: verum
end;
hence x in B ^Fob ; ::_thesis: verum
end;
theorem Th25: :: FINTOPO2:25
for FMT being non empty FMT_Space_Str
for A, B being Subset of FMT st A c= B holds
A ^Foi c= B ^Foi
proof
let FMT be non empty FMT_Space_Str ; ::_thesis: for A, B being Subset of FMT st A c= B holds
A ^Foi c= B ^Foi
let A, B be Subset of FMT; ::_thesis: ( A c= B implies A ^Foi c= B ^Foi )
assume A1: A c= B ; ::_thesis: A ^Foi c= B ^Foi
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A ^Foi or x in B ^Foi )
assume A2: x in A ^Foi ; ::_thesis: x in B ^Foi
then reconsider y = x as Element of FMT ;
consider V9 being Subset of FMT such that
A3: V9 in U_FMT y and
A4: V9 c= A by A2, Th21;
V9 c= B by A1, A4, XBOOLE_1:1;
hence x in B ^Foi by A3; ::_thesis: verum
end;
theorem Th26: :: FINTOPO2:26
for FMT being non empty FMT_Space_Str
for A, B being Subset of FMT holds (A ^Fob) \/ (B ^Fob) c= (A \/ B) ^Fob
proof
let FMT be non empty FMT_Space_Str ; ::_thesis: for A, B being Subset of FMT holds (A ^Fob) \/ (B ^Fob) c= (A \/ B) ^Fob
let A, B be Subset of FMT; ::_thesis: (A ^Fob) \/ (B ^Fob) c= (A \/ B) ^Fob
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A ^Fob) \/ (B ^Fob) or x in (A \/ B) ^Fob )
assume x in (A ^Fob) \/ (B ^Fob) ; ::_thesis: x in (A \/ B) ^Fob
then A1: ( x in A ^Fob or x in B ^Fob ) by XBOOLE_0:def_3;
( A ^Fob c= (A \/ B) ^Fob & B ^Fob c= (B \/ A) ^Fob ) by Th24, XBOOLE_1:7;
hence x in (A \/ B) ^Fob by A1; ::_thesis: verum
end;
theorem :: FINTOPO2:27
for FMT being non empty FMT_Space_Str
for A, B being Subset of FMT holds (A /\ B) ^Fob c= (A ^Fob) /\ (B ^Fob)
proof
let FMT be non empty FMT_Space_Str ; ::_thesis: for A, B being Subset of FMT holds (A /\ B) ^Fob c= (A ^Fob) /\ (B ^Fob)
let A, B be Subset of FMT; ::_thesis: (A /\ B) ^Fob c= (A ^Fob) /\ (B ^Fob)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A /\ B) ^Fob or x in (A ^Fob) /\ (B ^Fob) )
assume A1: x in (A /\ B) ^Fob ; ::_thesis: x in (A ^Fob) /\ (B ^Fob)
( (A /\ B) ^Fob c= A ^Fob & (B /\ A) ^Fob c= B ^Fob ) by Th24, XBOOLE_1:17;
hence x in (A ^Fob) /\ (B ^Fob) by A1, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem :: FINTOPO2:28
for FMT being non empty FMT_Space_Str
for A, B being Subset of FMT holds (A ^Foi) \/ (B ^Foi) c= (A \/ B) ^Foi
proof
let FMT be non empty FMT_Space_Str ; ::_thesis: for A, B being Subset of FMT holds (A ^Foi) \/ (B ^Foi) c= (A \/ B) ^Foi
let A, B be Subset of FMT; ::_thesis: (A ^Foi) \/ (B ^Foi) c= (A \/ B) ^Foi
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A ^Foi) \/ (B ^Foi) or x in (A \/ B) ^Foi )
assume x in (A ^Foi) \/ (B ^Foi) ; ::_thesis: x in (A \/ B) ^Foi
then A1: ( x in A ^Foi or x in B ^Foi ) by XBOOLE_0:def_3;
( A ^Foi c= (A \/ B) ^Foi & B ^Foi c= (B \/ A) ^Foi ) by Th25, XBOOLE_1:7;
hence x in (A \/ B) ^Foi by A1; ::_thesis: verum
end;
theorem Th29: :: FINTOPO2:29
for FMT being non empty FMT_Space_Str
for A, B being Subset of FMT holds (A /\ B) ^Foi c= (A ^Foi) /\ (B ^Foi)
proof
let FMT be non empty FMT_Space_Str ; ::_thesis: for A, B being Subset of FMT holds (A /\ B) ^Foi c= (A ^Foi) /\ (B ^Foi)
let A, B be Subset of FMT; ::_thesis: (A /\ B) ^Foi c= (A ^Foi) /\ (B ^Foi)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A /\ B) ^Foi or x in (A ^Foi) /\ (B ^Foi) )
assume A1: x in (A /\ B) ^Foi ; ::_thesis: x in (A ^Foi) /\ (B ^Foi)
( (A /\ B) ^Foi c= A ^Foi & (B /\ A) ^Foi c= B ^Foi ) by Th25, XBOOLE_1:17;
hence x in (A ^Foi) /\ (B ^Foi) by A1, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem :: FINTOPO2:30
for FMT being non empty FMT_Space_Str holds
( ( for x being Element of FMT
for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds
ex W being Subset of FMT st
( W in U_FMT x & W c= V1 /\ V2 ) ) iff for A, B being Subset of FMT holds (A \/ B) ^Fob = (A ^Fob) \/ (B ^Fob) )
proof
let FMT be non empty FMT_Space_Str ; ::_thesis: ( ( for x being Element of FMT
for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds
ex W being Subset of FMT st
( W in U_FMT x & W c= V1 /\ V2 ) ) iff for A, B being Subset of FMT holds (A \/ B) ^Fob = (A ^Fob) \/ (B ^Fob) )
A1: ( ( for x being Element of FMT
for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds
ex W being Subset of FMT st
( W in U_FMT x & W c= V1 /\ V2 ) ) implies for A, B being Subset of FMT holds (A \/ B) ^Fob = (A ^Fob) \/ (B ^Fob) )
proof
assume A2: for x being Element of FMT
for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds
ex W being Subset of FMT st
( W in U_FMT x & W c= V1 /\ V2 ) ; ::_thesis: for A, B being Subset of FMT holds (A \/ B) ^Fob = (A ^Fob) \/ (B ^Fob)
let A, B be Subset of FMT; ::_thesis: (A \/ B) ^Fob = (A ^Fob) \/ (B ^Fob)
for x being Element of FMT holds
( x in (A \/ B) ^Fob iff x in (A ^Fob) \/ (B ^Fob) )
proof
let x be Element of FMT; ::_thesis: ( x in (A \/ B) ^Fob iff x in (A ^Fob) \/ (B ^Fob) )
A3: ( x in (A \/ B) ^Fob implies x in (A ^Fob) \/ (B ^Fob) )
proof
assume A4: x in (A \/ B) ^Fob ; ::_thesis: x in (A ^Fob) \/ (B ^Fob)
A5: for W1 being Subset of FMT holds
( not W1 in U_FMT x or W1 meets A or W1 meets B )
proof
let W1 be Subset of FMT; ::_thesis: ( not W1 in U_FMT x or W1 meets A or W1 meets B )
assume W1 in U_FMT x ; ::_thesis: ( W1 meets A or W1 meets B )
then W1 meets A \/ B by A4, Th20;
then W1 /\ (A \/ B) <> {} by XBOOLE_0:def_7;
then (W1 /\ A) \/ (W1 /\ B) <> {} by XBOOLE_1:23;
then ( W1 /\ A <> {} or W1 /\ B <> {} ) ;
hence ( W1 meets A or W1 meets B ) by XBOOLE_0:def_7; ::_thesis: verum
end;
for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x & not V1 meets A holds
V2 meets B
proof
let V1, V2 be Subset of FMT; ::_thesis: ( V1 in U_FMT x & V2 in U_FMT x & not V1 meets A implies V2 meets B )
assume ( V1 in U_FMT x & V2 in U_FMT x ) ; ::_thesis: ( V1 meets A or V2 meets B )
then consider W being Subset of FMT such that
A6: W in U_FMT x and
A7: W c= V1 /\ V2 by A2;
V1 /\ V2 c= V1 by XBOOLE_1:17;
then W c= V1 by A7, XBOOLE_1:1;
then A8: W /\ A c= V1 /\ A by XBOOLE_1:26;
V1 /\ V2 c= V2 by XBOOLE_1:17;
then W c= V2 by A7, XBOOLE_1:1;
then A9: W /\ B c= V2 /\ B by XBOOLE_1:26;
( W meets A or W meets B ) by A5, A6;
then ( W /\ A <> {} or W /\ B <> {} ) by XBOOLE_0:def_7;
then ex z1, z2 being Element of FMT st
( z1 in W /\ A or z2 in W /\ B ) by SUBSET_1:4;
hence ( V1 meets A or V2 meets B ) by A8, A9, XBOOLE_0:def_7; ::_thesis: verum
end;
then ( for V1 being Subset of FMT st V1 in U_FMT x holds
V1 meets A or for V2 being Subset of FMT st V2 in U_FMT x holds
V2 meets B ) ;
then ( x in A ^Fob or x in B ^Fob ) ;
hence x in (A ^Fob) \/ (B ^Fob) by XBOOLE_0:def_3; ::_thesis: verum
end;
( x in (A ^Fob) \/ (B ^Fob) implies x in (A \/ B) ^Fob )
proof
assume A10: x in (A ^Fob) \/ (B ^Fob) ; ::_thesis: x in (A \/ B) ^Fob
(A ^Fob) \/ (B ^Fob) c= (A \/ B) ^Fob by Th26;
hence x in (A \/ B) ^Fob by A10; ::_thesis: verum
end;
hence ( x in (A \/ B) ^Fob iff x in (A ^Fob) \/ (B ^Fob) ) by A3; ::_thesis: verum
end;
hence (A \/ B) ^Fob = (A ^Fob) \/ (B ^Fob) by SUBSET_1:3; ::_thesis: verum
end;
( ex x being Element of FMT ex V1, V2 being Subset of FMT st
( V1 in U_FMT x & V2 in U_FMT x & ( for W being Subset of FMT st W in U_FMT x holds
not W c= V1 /\ V2 ) ) implies ex A, B being Subset of FMT st (A \/ B) ^Fob <> (A ^Fob) \/ (B ^Fob) )
proof
given x0 being Element of FMT, V1, V2 being Subset of FMT such that A11: V1 in U_FMT x0 and
A12: V2 in U_FMT x0 and
A13: for W being Subset of FMT st W in U_FMT x0 holds
not W c= V1 /\ V2 ; ::_thesis: ex A, B being Subset of FMT st (A \/ B) ^Fob <> (A ^Fob) \/ (B ^Fob)
A14: not x0 in (V2 `) ^Fob
proof
A15: V2 misses V2 ` by XBOOLE_1:79;
assume x0 in (V2 `) ^Fob ; ::_thesis: contradiction
hence contradiction by A12, A15, Th20; ::_thesis: verum
end;
take V1 ` ; ::_thesis: ex B being Subset of FMT st ((V1 `) \/ B) ^Fob <> ((V1 `) ^Fob) \/ (B ^Fob)
take V2 ` ; ::_thesis: ((V1 `) \/ (V2 `)) ^Fob <> ((V1 `) ^Fob) \/ ((V2 `) ^Fob)
for W being Subset of FMT st W in U_FMT x0 holds
W meets (V1 `) \/ (V2 `)
proof
let W be Subset of FMT; ::_thesis: ( W in U_FMT x0 implies W meets (V1 `) \/ (V2 `) )
assume W in U_FMT x0 ; ::_thesis: W meets (V1 `) \/ (V2 `)
then A16: not W c= V1 /\ V2 by A13;
W /\ ((V1 /\ V2) `) <> {}
proof
assume W /\ ((V1 /\ V2) `) = {} ; ::_thesis: contradiction
then W \ (V1 /\ V2) = {} by SUBSET_1:13;
hence contradiction by A16, XBOOLE_1:37; ::_thesis: verum
end;
hence W /\ ((V1 `) \/ (V2 `)) <> {} by XBOOLE_1:54; :: according to XBOOLE_0:def_7 ::_thesis: verum
end;
then A17: x0 in ((V1 `) \/ (V2 `)) ^Fob ;
not x0 in (V1 `) ^Fob
proof
A18: V1 misses V1 ` by XBOOLE_1:79;
assume x0 in (V1 `) ^Fob ; ::_thesis: contradiction
hence contradiction by A11, A18, Th20; ::_thesis: verum
end;
hence ((V1 `) \/ (V2 `)) ^Fob <> ((V1 `) ^Fob) \/ ((V2 `) ^Fob) by A17, A14, XBOOLE_0:def_3; ::_thesis: verum
end;
hence ( ( for x being Element of FMT
for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds
ex W being Subset of FMT st
( W in U_FMT x & W c= V1 /\ V2 ) ) iff for A, B being Subset of FMT holds (A \/ B) ^Fob = (A ^Fob) \/ (B ^Fob) ) by A1; ::_thesis: verum
end;
theorem :: FINTOPO2:31
for FMT being non empty FMT_Space_Str holds
( ( for x being Element of FMT
for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds
ex W being Subset of FMT st
( W in U_FMT x & W c= V1 /\ V2 ) ) iff for A, B being Subset of FMT holds (A ^Foi) /\ (B ^Foi) = (A /\ B) ^Foi )
proof
let FMT be non empty FMT_Space_Str ; ::_thesis: ( ( for x being Element of FMT
for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds
ex W being Subset of FMT st
( W in U_FMT x & W c= V1 /\ V2 ) ) iff for A, B being Subset of FMT holds (A ^Foi) /\ (B ^Foi) = (A /\ B) ^Foi )
thus ( ( for x being Element of FMT
for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds
ex W being Subset of FMT st
( W in U_FMT x & W c= V1 /\ V2 ) ) implies for A, B being Subset of FMT holds (A ^Foi) /\ (B ^Foi) = (A /\ B) ^Foi ) ::_thesis: ( ( for A, B being Subset of FMT holds (A ^Foi) /\ (B ^Foi) = (A /\ B) ^Foi ) implies for x being Element of FMT
for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds
ex W being Subset of FMT st
( W in U_FMT x & W c= V1 /\ V2 ) )
proof
assume A1: for x being Element of FMT
for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds
ex W being Subset of FMT st
( W in U_FMT x & W c= V1 /\ V2 ) ; ::_thesis: for A, B being Subset of FMT holds (A ^Foi) /\ (B ^Foi) = (A /\ B) ^Foi
let A, B be Subset of FMT; ::_thesis: (A ^Foi) /\ (B ^Foi) = (A /\ B) ^Foi
for x being Element of FMT holds
( x in (A ^Foi) /\ (B ^Foi) iff x in (A /\ B) ^Foi )
proof
let x be Element of FMT; ::_thesis: ( x in (A ^Foi) /\ (B ^Foi) iff x in (A /\ B) ^Foi )
A2: ( x in (A ^Foi) /\ (B ^Foi) implies x in (A /\ B) ^Foi )
proof
assume A3: x in (A ^Foi) /\ (B ^Foi) ; ::_thesis: x in (A /\ B) ^Foi
then x in B ^Foi by XBOOLE_0:def_4;
then A4: ex W2 being Subset of FMT st
( W2 in U_FMT x & W2 c= B ) by Th21;
x in A ^Foi by A3, XBOOLE_0:def_4;
then ex W1 being Subset of FMT st
( W1 in U_FMT x & W1 c= A ) by Th21;
then consider W1, W2 being Subset of FMT such that
A5: ( W1 in U_FMT x & W2 in U_FMT x ) and
A6: W1 c= A and
A7: W2 c= B by A4;
consider W being Subset of FMT such that
A8: W in U_FMT x and
A9: W c= W1 /\ W2 by A1, A5;
W1 /\ W2 c= W2 by XBOOLE_1:17;
then W c= W2 by A9, XBOOLE_1:1;
then A10: W c= B by A7, XBOOLE_1:1;
W1 /\ W2 c= W1 by XBOOLE_1:17;
then W c= W1 by A9, XBOOLE_1:1;
then W c= A by A6, XBOOLE_1:1;
then W c= A /\ B by A10, XBOOLE_1:19;
hence x in (A /\ B) ^Foi by A8; ::_thesis: verum
end;
( x in (A /\ B) ^Foi implies x in (A ^Foi) /\ (B ^Foi) )
proof
assume A11: x in (A /\ B) ^Foi ; ::_thesis: x in (A ^Foi) /\ (B ^Foi)
(A /\ B) ^Foi c= (A ^Foi) /\ (B ^Foi) by Th29;
hence x in (A ^Foi) /\ (B ^Foi) by A11; ::_thesis: verum
end;
hence ( x in (A ^Foi) /\ (B ^Foi) iff x in (A /\ B) ^Foi ) by A2; ::_thesis: verum
end;
hence (A ^Foi) /\ (B ^Foi) = (A /\ B) ^Foi by SUBSET_1:3; ::_thesis: verum
end;
( ex x being Element of FMT ex V1, V2 being Subset of FMT st
( V1 in U_FMT x & V2 in U_FMT x & ( for W being Subset of FMT st W in U_FMT x holds
not W c= V1 /\ V2 ) ) implies ex A, B being Subset of FMT st (A ^Foi) /\ (B ^Foi) <> (A /\ B) ^Foi )
proof
given x0 being Element of FMT, V1, V2 being Subset of FMT such that A12: ( V1 in U_FMT x0 & V2 in U_FMT x0 ) and
A13: for W being Subset of FMT st W in U_FMT x0 holds
not W c= V1 /\ V2 ; ::_thesis: ex A, B being Subset of FMT st (A ^Foi) /\ (B ^Foi) <> (A /\ B) ^Foi
take V1 ; ::_thesis: ex B being Subset of FMT st (V1 ^Foi) /\ (B ^Foi) <> (V1 /\ B) ^Foi
take V2 ; ::_thesis: (V1 ^Foi) /\ (V2 ^Foi) <> (V1 /\ V2) ^Foi
( x0 in V1 ^Foi & x0 in V2 ^Foi ) by A12;
then x0 in (V1 ^Foi) /\ (V2 ^Foi) by XBOOLE_0:def_4;
hence (V1 ^Foi) /\ (V2 ^Foi) <> (V1 /\ V2) ^Foi by A13, Th21; ::_thesis: verum
end;
hence ( ( for A, B being Subset of FMT holds (A ^Foi) /\ (B ^Foi) = (A /\ B) ^Foi ) implies for x being Element of FMT
for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds
ex W being Subset of FMT st
( W in U_FMT x & W c= V1 /\ V2 ) ) ; ::_thesis: verum
end;
theorem :: FINTOPO2:32
for FMT being non empty FMT_Space_Str
for A, B being Subset of FMT st ( for x being Element of FMT
for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds
ex W being Subset of FMT st
( W in U_FMT x & W c= V1 /\ V2 ) ) holds
(A \/ B) ^Fodelta c= (A ^Fodelta) \/ (B ^Fodelta)
proof
let FMT be non empty FMT_Space_Str ; ::_thesis: for A, B being Subset of FMT st ( for x being Element of FMT
for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds
ex W being Subset of FMT st
( W in U_FMT x & W c= V1 /\ V2 ) ) holds
(A \/ B) ^Fodelta c= (A ^Fodelta) \/ (B ^Fodelta)
let A, B be Subset of FMT; ::_thesis: ( ( for x being Element of FMT
for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds
ex W being Subset of FMT st
( W in U_FMT x & W c= V1 /\ V2 ) ) implies (A \/ B) ^Fodelta c= (A ^Fodelta) \/ (B ^Fodelta) )
assume A1: for x being Element of FMT
for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds
ex W being Subset of FMT st
( W in U_FMT x & W c= V1 /\ V2 ) ; ::_thesis: (A \/ B) ^Fodelta c= (A ^Fodelta) \/ (B ^Fodelta)
for x being Element of FMT st x in (A \/ B) ^Fodelta holds
x in (A ^Fodelta) \/ (B ^Fodelta)
proof
let x be Element of FMT; ::_thesis: ( x in (A \/ B) ^Fodelta implies x in (A ^Fodelta) \/ (B ^Fodelta) )
assume A2: x in (A \/ B) ^Fodelta ; ::_thesis: x in (A ^Fodelta) \/ (B ^Fodelta)
A3: for W1 being Subset of FMT holds
( not W1 in U_FMT x or ( W1 meets A & W1 meets A ` ) or ( W1 meets B & W1 meets B ` ) )
proof
let W1 be Subset of FMT; ::_thesis: ( not W1 in U_FMT x or ( W1 meets A & W1 meets A ` ) or ( W1 meets B & W1 meets B ` ) )
assume A4: W1 in U_FMT x ; ::_thesis: ( ( W1 meets A & W1 meets A ` ) or ( W1 meets B & W1 meets B ` ) )
then W1 meets (A \/ B) ` by A2, Th19;
then W1 /\ ((A \/ B) `) <> {} by XBOOLE_0:def_7;
then A5: W1 /\ ((A `) /\ (B `)) <> {} by XBOOLE_1:53;
then (W1 /\ (A `)) /\ (B `) <> {} by XBOOLE_1:16;
then W1 /\ (A `) meets B ` by XBOOLE_0:def_7;
then A6: ex z1 being set st z1 in (W1 /\ (A `)) /\ (B `) by XBOOLE_0:4;
(W1 /\ (B `)) /\ (A `) <> {} by A5, XBOOLE_1:16;
then W1 /\ (B `) meets A ` by XBOOLE_0:def_7;
then A7: ex z2 being set st z2 in (W1 /\ (B `)) /\ (A `) by XBOOLE_0:4;
W1 meets A \/ B by A2, A4, Th19;
then W1 /\ (A \/ B) <> {} by XBOOLE_0:def_7;
then (W1 /\ A) \/ (W1 /\ B) <> {} by XBOOLE_1:23;
then ( ( W1 /\ A <> {} & W1 /\ (A `) <> {} ) or ( W1 /\ B <> {} & W1 /\ (B `) <> {} ) ) by A6, A7;
hence ( ( W1 meets A & W1 meets A ` ) or ( W1 meets B & W1 meets B ` ) ) by XBOOLE_0:def_7; ::_thesis: verum
end;
for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x & not ( V1 meets A & V1 meets A ` ) holds
( V2 meets B & V2 meets B ` )
proof
let V1, V2 be Subset of FMT; ::_thesis: ( V1 in U_FMT x & V2 in U_FMT x & not ( V1 meets A & V1 meets A ` ) implies ( V2 meets B & V2 meets B ` ) )
assume ( V1 in U_FMT x & V2 in U_FMT x ) ; ::_thesis: ( ( V1 meets A & V1 meets A ` ) or ( V2 meets B & V2 meets B ` ) )
then consider W being Subset of FMT such that
A8: W in U_FMT x and
A9: W c= V1 /\ V2 by A1;
V1 /\ V2 c= V2 by XBOOLE_1:17;
then W c= V2 by A9, XBOOLE_1:1;
then A10: ( W /\ B c= V2 /\ B & W /\ (B `) c= V2 /\ (B `) ) by XBOOLE_1:26;
V1 /\ V2 c= V1 by XBOOLE_1:17;
then W c= V1 by A9, XBOOLE_1:1;
then A11: ( W /\ A c= V1 /\ A & W /\ (A `) c= V1 /\ (A `) ) by XBOOLE_1:26;
( ( V1 meets A & V1 meets A ` ) or ( V2 meets B & V2 meets B ` ) )
proof
now__::_thesis:_(_(_W_meets_A_&_W_meets_A_`_&_(_(_V1_meets_A_&_V1_meets_A_`_)_or_(_V2_meets_B_&_V2_meets_B_`_)_)_)_or_(_W_meets_B_&_W_meets_B_`_&_(_(_V1_meets_A_&_V1_meets_A_`_)_or_(_V2_meets_B_&_V2_meets_B_`_)_)_)_)
percases ( ( W meets A & W meets A ` ) or ( W meets B & W meets B ` ) ) by A3, A8;
case ( W meets A & W meets A ` ) ; ::_thesis: ( ( V1 meets A & V1 meets A ` ) or ( V2 meets B & V2 meets B ` ) )
then ( ex z1 being set st z1 in W /\ A & ex z2 being set st z2 in W /\ (A `) ) by XBOOLE_0:4;
hence ( ( V1 meets A & V1 meets A ` ) or ( V2 meets B & V2 meets B ` ) ) by A11, XBOOLE_0:4; ::_thesis: verum
end;
case ( W meets B & W meets B ` ) ; ::_thesis: ( ( V1 meets A & V1 meets A ` ) or ( V2 meets B & V2 meets B ` ) )
then ( ex z3 being set st z3 in W /\ B & ex z4 being set st z4 in W /\ (B `) ) by XBOOLE_0:4;
hence ( ( V1 meets A & V1 meets A ` ) or ( V2 meets B & V2 meets B ` ) ) by A10, XBOOLE_0:4; ::_thesis: verum
end;
end;
end;
hence ( ( V1 meets A & V1 meets A ` ) or ( V2 meets B & V2 meets B ` ) ) ; ::_thesis: verum
end;
hence ( ( V1 meets A & V1 meets A ` ) or ( V2 meets B & V2 meets B ` ) ) ; ::_thesis: verum
end;
then ( for V1 being Subset of FMT st V1 in U_FMT x holds
( V1 meets A & V1 meets A ` ) or for V2 being Subset of FMT st V2 in U_FMT x holds
( V2 meets B & V2 meets B ` ) ) ;
then ( x in A ^Fodelta or x in B ^Fodelta ) ;
hence x in (A ^Fodelta) \/ (B ^Fodelta) by XBOOLE_0:def_3; ::_thesis: verum
end;
hence (A \/ B) ^Fodelta c= (A ^Fodelta) \/ (B ^Fodelta) by SUBSET_1:2; ::_thesis: verum
end;
theorem :: FINTOPO2:33
for FMT being non empty FMT_Space_Str st FMT is Fo_filled & ( for A, B being Subset of FMT holds (A \/ B) ^Fodelta = (A ^Fodelta) \/ (B ^Fodelta) ) holds
for x being Element of FMT
for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds
ex W being Subset of FMT st
( W in U_FMT x & W c= V1 /\ V2 )
proof
let FMT be non empty FMT_Space_Str ; ::_thesis: ( FMT is Fo_filled & ( for A, B being Subset of FMT holds (A \/ B) ^Fodelta = (A ^Fodelta) \/ (B ^Fodelta) ) implies for x being Element of FMT
for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds
ex W being Subset of FMT st
( W in U_FMT x & W c= V1 /\ V2 ) )
assume A1: FMT is Fo_filled ; ::_thesis: ( ex A, B being Subset of FMT st not (A \/ B) ^Fodelta = (A ^Fodelta) \/ (B ^Fodelta) or for x being Element of FMT
for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds
ex W being Subset of FMT st
( W in U_FMT x & W c= V1 /\ V2 ) )
( ex x being Element of FMT ex V1, V2 being Subset of FMT st
( V1 in U_FMT x & V2 in U_FMT x & ( for W being Subset of FMT st W in U_FMT x holds
not W c= V1 /\ V2 ) ) implies ex A, B being Subset of FMT st (A \/ B) ^Fodelta <> (A ^Fodelta) \/ (B ^Fodelta) )
proof
given x0 being Element of FMT, V1, V2 being Subset of FMT such that A2: V1 in U_FMT x0 and
A3: V2 in U_FMT x0 and
A4: for W being Subset of FMT st W in U_FMT x0 holds
not W c= V1 /\ V2 ; ::_thesis: ex A, B being Subset of FMT st (A \/ B) ^Fodelta <> (A ^Fodelta) \/ (B ^Fodelta)
take V1 ` ; ::_thesis: ex B being Subset of FMT st ((V1 `) \/ B) ^Fodelta <> ((V1 `) ^Fodelta) \/ (B ^Fodelta)
take V2 ` ; ::_thesis: ((V1 `) \/ (V2 `)) ^Fodelta <> ((V1 `) ^Fodelta) \/ ((V2 `) ^Fodelta)
A5: not x0 in (V2 `) ^Fodelta
proof
assume x0 in (V2 `) ^Fodelta ; ::_thesis: contradiction
then V2 meets V2 ` by A3, Th19;
hence contradiction by XBOOLE_1:79; ::_thesis: verum
end;
for W being Subset of FMT st W in U_FMT x0 holds
( W meets (V1 `) \/ (V2 `) & W meets ((V1 `) \/ (V2 `)) ` )
proof
let W be Subset of FMT; ::_thesis: ( W in U_FMT x0 implies ( W meets (V1 `) \/ (V2 `) & W meets ((V1 `) \/ (V2 `)) ` ) )
assume A6: W in U_FMT x0 ; ::_thesis: ( W meets (V1 `) \/ (V2 `) & W meets ((V1 `) \/ (V2 `)) ` )
then A7: not W c= V1 /\ V2 by A4;
A8: W meets (V1 /\ V2) `
proof
assume W /\ ((V1 /\ V2) `) = {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
then W \ (V1 /\ V2) = {} by SUBSET_1:13;
hence contradiction by A7, XBOOLE_1:37; ::_thesis: verum
end;
( x0 in V1 & x0 in V2 ) by A1, A2, A3, Def8;
then A9: x0 in V1 /\ V2 by XBOOLE_0:def_4;
x0 in W by A1, A6, Def8;
then W /\ (((V1 /\ V2) `) `) <> {} by A9, XBOOLE_0:def_4;
then W meets ((V1 /\ V2) `) ` by XBOOLE_0:def_7;
hence ( W meets (V1 `) \/ (V2 `) & W meets ((V1 `) \/ (V2 `)) ` ) by A8, XBOOLE_1:54; ::_thesis: verum
end;
then A10: x0 in ((V1 `) \/ (V2 `)) ^Fodelta ;
not x0 in (V1 `) ^Fodelta
proof
assume x0 in (V1 `) ^Fodelta ; ::_thesis: contradiction
then V1 meets V1 ` by A2, Th19;
hence contradiction by XBOOLE_1:79; ::_thesis: verum
end;
hence ((V1 `) \/ (V2 `)) ^Fodelta <> ((V1 `) ^Fodelta) \/ ((V2 `) ^Fodelta) by A10, A5, XBOOLE_0:def_3; ::_thesis: verum
end;
hence ( ex A, B being Subset of FMT st not (A \/ B) ^Fodelta = (A ^Fodelta) \/ (B ^Fodelta) or for x being Element of FMT
for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds
ex W being Subset of FMT st
( W in U_FMT x & W c= V1 /\ V2 ) ) ; ::_thesis: verum
end;
theorem :: FINTOPO2:34
for FMT being non empty FMT_Space_Str
for x being Element of FMT
for A being Subset of FMT holds
( x in A ^Fos iff ( x in A & not x in (A \ {x}) ^Fob ) )
proof
let FMT be non empty FMT_Space_Str ; ::_thesis: for x being Element of FMT
for A being Subset of FMT holds
( x in A ^Fos iff ( x in A & not x in (A \ {x}) ^Fob ) )
let x be Element of FMT; ::_thesis: for A being Subset of FMT holds
( x in A ^Fos iff ( x in A & not x in (A \ {x}) ^Fob ) )
let A be Subset of FMT; ::_thesis: ( x in A ^Fos iff ( x in A & not x in (A \ {x}) ^Fob ) )
A1: ( x in A & not x in (A \ {x}) ^Fob implies x in A ^Fos )
proof
assume that
A2: x in A and
A3: not x in (A \ {x}) ^Fob ; ::_thesis: x in A ^Fos
consider V9 being Subset of FMT such that
A4: V9 in U_FMT x and
A5: V9 misses A \ {x} by A3;
V9 misses A /\ ({x} `) by A5, SUBSET_1:13;
then V9 /\ (A /\ ({x} `)) = {} by XBOOLE_0:def_7;
then (V9 /\ ({x} `)) /\ A = {} by XBOOLE_1:16;
then (V9 \ {x}) /\ A = {} by SUBSET_1:13;
then V9 \ {x} misses A by XBOOLE_0:def_7;
hence x in A ^Fos by A2, A4; ::_thesis: verum
end;
( x in A ^Fos implies ( x in A & not x in (A \ {x}) ^Fob ) )
proof
assume A6: x in A ^Fos ; ::_thesis: ( x in A & not x in (A \ {x}) ^Fob )
then consider V9 being Subset of FMT such that
A7: V9 in U_FMT x and
A8: V9 \ {x} misses A by Th22;
V9 /\ ({x} `) misses A by A8, SUBSET_1:13;
then (V9 /\ ({x} `)) /\ A = {} by XBOOLE_0:def_7;
then V9 /\ (({x} `) /\ A) = {} by XBOOLE_1:16;
then V9 misses ({x} `) /\ A by XBOOLE_0:def_7;
then V9 misses A \ {x} by SUBSET_1:13;
hence ( x in A & not x in (A \ {x}) ^Fob ) by A6, A7, Th20, Th22; ::_thesis: verum
end;
hence ( x in A ^Fos iff ( x in A & not x in (A \ {x}) ^Fob ) ) by A1; ::_thesis: verum
end;
theorem Th35: :: FINTOPO2:35
for FMT being non empty FMT_Space_Str holds
( FMT is Fo_filled iff for A being Subset of FMT holds A c= A ^Fob )
proof
let FMT be non empty FMT_Space_Str ; ::_thesis: ( FMT is Fo_filled iff for A being Subset of FMT holds A c= A ^Fob )
A1: ( ( for A being Subset of FMT holds A c= A ^Fob ) implies FMT is Fo_filled )
proof
assume A2: for A being Subset of FMT holds A c= A ^Fob ; ::_thesis: FMT is Fo_filled
assume not FMT is Fo_filled ; ::_thesis: contradiction
then consider y being Element of FMT, V being Subset of FMT such that
A3: V in U_FMT y and
A4: not y in V by Def8;
A5: V misses {y}
proof
assume V meets {y} ; ::_thesis: contradiction
then ex z being set st
( z in V & z in {y} ) by XBOOLE_0:3;
hence contradiction by A4, TARSKI:def_1; ::_thesis: verum
end;
not {y} c= {y} ^Fob
proof
A6: y in {y} by TARSKI:def_1;
assume {y} c= {y} ^Fob ; ::_thesis: contradiction
hence contradiction by A3, A5, A6, Th20; ::_thesis: verum
end;
hence contradiction by A2; ::_thesis: verum
end;
( FMT is Fo_filled implies for A being Subset of FMT holds A c= A ^Fob )
proof
assume A7: FMT is Fo_filled ; ::_thesis: for A being Subset of FMT holds A c= A ^Fob
let A be Subset of FMT; ::_thesis: A c= A ^Fob
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in A ^Fob )
assume A8: x in A ; ::_thesis: x in A ^Fob
then reconsider y = x as Element of FMT ;
for W being Subset of FMT st W in U_FMT y holds
W meets A
proof
let W be Subset of FMT; ::_thesis: ( W in U_FMT y implies W meets A )
assume W in U_FMT y ; ::_thesis: W meets A
then y in W by A7, Def8;
hence W meets A by A8, XBOOLE_0:3; ::_thesis: verum
end;
hence x in A ^Fob ; ::_thesis: verum
end;
hence ( FMT is Fo_filled iff for A being Subset of FMT holds A c= A ^Fob ) by A1; ::_thesis: verum
end;
theorem Th36: :: FINTOPO2:36
for FMT being non empty FMT_Space_Str holds
( FMT is Fo_filled iff for A being Subset of FMT holds A ^Foi c= A )
proof
let FMT be non empty FMT_Space_Str ; ::_thesis: ( FMT is Fo_filled iff for A being Subset of FMT holds A ^Foi c= A )
A1: ( FMT is Fo_filled implies for A being Subset of FMT holds A ^Foi c= A )
proof
assume A2: FMT is Fo_filled ; ::_thesis: for A being Subset of FMT holds A ^Foi c= A
let A be Subset of FMT; ::_thesis: A ^Foi c= A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A ^Foi or x in A )
assume A3: x in A ^Foi ; ::_thesis: x in A
then reconsider y = x as Element of FMT ;
consider V being Subset of FMT such that
A4: V in U_FMT y and
A5: V c= A by A3, Th21;
y in V by A2, A4, Def8;
hence x in A by A5; ::_thesis: verum
end;
( ( for A being Subset of FMT holds A ^Foi c= A ) implies FMT is Fo_filled )
proof
assume A6: for A being Subset of FMT holds A ^Foi c= A ; ::_thesis: FMT is Fo_filled
assume not FMT is Fo_filled ; ::_thesis: contradiction
then consider y being Element of FMT, V being Subset of FMT such that
A7: V in U_FMT y and
A8: not y in V by Def8;
y in V ^Foi by A7;
then not V ^Foi c= V by A8;
hence contradiction by A6; ::_thesis: verum
end;
hence ( FMT is Fo_filled iff for A being Subset of FMT holds A ^Foi c= A ) by A1; ::_thesis: verum
end;
theorem Th37: :: FINTOPO2:37
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds ((A `) ^Fob) ` = A ^Foi
proof
let FMT be non empty FMT_Space_Str ; ::_thesis: for A being Subset of FMT holds ((A `) ^Fob) ` = A ^Foi
let A be Subset of FMT; ::_thesis: ((A `) ^Fob) ` = A ^Foi
for x being set holds
( x in ((A `) ^Fob) ` iff x in A ^Foi )
proof
let x be set ; ::_thesis: ( x in ((A `) ^Fob) ` iff x in A ^Foi )
thus ( x in ((A `) ^Fob) ` implies x in A ^Foi ) ::_thesis: ( x in A ^Foi implies x in ((A `) ^Fob) ` )
proof
assume A1: x in ((A `) ^Fob) ` ; ::_thesis: x in A ^Foi
then reconsider y = x as Element of FMT ;
not y in (A `) ^Fob by A1, XBOOLE_0:def_5;
then consider V being Subset of FMT such that
A2: V in U_FMT y and
A3: V misses A ` ;
V /\ (A `) = {} by A3, XBOOLE_0:def_7;
then V \ A = {} by SUBSET_1:13;
then V c= A by XBOOLE_1:37;
hence x in A ^Foi by A2; ::_thesis: verum
end;
assume A4: x in A ^Foi ; ::_thesis: x in ((A `) ^Fob) `
then reconsider y = x as Element of FMT ;
consider V being Subset of FMT such that
A5: V in U_FMT y and
A6: V c= A by A4, Th21;
V \ A = {} by A6, XBOOLE_1:37;
then V /\ (A `) = {} by SUBSET_1:13;
then V misses A ` by XBOOLE_0:def_7;
then not y in (A `) ^Fob by A5, Th20;
hence x in ((A `) ^Fob) ` by XBOOLE_0:def_5; ::_thesis: verum
end;
hence ((A `) ^Fob) ` = A ^Foi by TARSKI:1; ::_thesis: verum
end;
theorem Th38: :: FINTOPO2:38
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds ((A `) ^Foi) ` = A ^Fob
proof
let FMT be non empty FMT_Space_Str ; ::_thesis: for A being Subset of FMT holds ((A `) ^Foi) ` = A ^Fob
let A be Subset of FMT; ::_thesis: ((A `) ^Foi) ` = A ^Fob
for x being set holds
( x in ((A `) ^Foi) ` iff x in A ^Fob )
proof
let x be set ; ::_thesis: ( x in ((A `) ^Foi) ` iff x in A ^Fob )
thus ( x in ((A `) ^Foi) ` implies x in A ^Fob ) ::_thesis: ( x in A ^Fob implies x in ((A `) ^Foi) ` )
proof
assume A1: x in ((A `) ^Foi) ` ; ::_thesis: x in A ^Fob
then reconsider y = x as Element of FMT ;
A2: not y in (A `) ^Foi by A1, XBOOLE_0:def_5;
for W being Subset of FMT st W in U_FMT y holds
W meets A
proof
let W be Subset of FMT; ::_thesis: ( W in U_FMT y implies W meets A )
assume W in U_FMT y ; ::_thesis: W meets A
then not W c= A ` by A2;
then consider z being set such that
A3: z in W and
A4: not z in A ` by TARSKI:def_3;
z in A by A3, A4, XBOOLE_0:def_5;
hence W meets A by A3, XBOOLE_0:3; ::_thesis: verum
end;
hence x in A ^Fob ; ::_thesis: verum
end;
assume A5: x in A ^Fob ; ::_thesis: x in ((A `) ^Foi) `
then reconsider y = x as Element of FMT ;
for W being Subset of FMT st W in U_FMT y holds
not W c= A `
proof
let W be Subset of FMT; ::_thesis: ( W in U_FMT y implies not W c= A ` )
assume W in U_FMT y ; ::_thesis: not W c= A `
then W meets A by A5, Th20;
then ex z being set st
( z in W & z in A ) by XBOOLE_0:3;
hence not W c= A ` by XBOOLE_0:def_5; ::_thesis: verum
end;
then not y in (A `) ^Foi by Th21;
hence x in ((A `) ^Foi) ` by XBOOLE_0:def_5; ::_thesis: verum
end;
hence ((A `) ^Foi) ` = A ^Fob by TARSKI:1; ::_thesis: verum
end;
theorem Th39: :: FINTOPO2:39
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Fodelta = (A ^Fob) /\ ((A `) ^Fob)
proof
let FMT be non empty FMT_Space_Str ; ::_thesis: for A being Subset of FMT holds A ^Fodelta = (A ^Fob) /\ ((A `) ^Fob)
let A be Subset of FMT; ::_thesis: A ^Fodelta = (A ^Fob) /\ ((A `) ^Fob)
for x being Element of FMT holds
( x in A ^Fodelta iff x in (A ^Fob) /\ ((A `) ^Fob) )
proof
let x be Element of FMT; ::_thesis: ( x in A ^Fodelta iff x in (A ^Fob) /\ ((A `) ^Fob) )
thus ( x in A ^Fodelta implies x in (A ^Fob) /\ ((A `) ^Fob) ) ::_thesis: ( x in (A ^Fob) /\ ((A `) ^Fob) implies x in A ^Fodelta )
proof
assume A1: x in A ^Fodelta ; ::_thesis: x in (A ^Fob) /\ ((A `) ^Fob)
then for W being Subset of FMT st W in U_FMT x holds
W meets A ` by Th19;
then A2: x in (A `) ^Fob ;
for W being Subset of FMT st W in U_FMT x holds
W meets A by A1, Th19;
then x in A ^Fob ;
hence x in (A ^Fob) /\ ((A `) ^Fob) by A2, XBOOLE_0:def_4; ::_thesis: verum
end;
assume x in (A ^Fob) /\ ((A `) ^Fob) ; ::_thesis: x in A ^Fodelta
then ( x in A ^Fob & x in (A `) ^Fob ) by XBOOLE_0:def_4;
then for W being Subset of FMT st W in U_FMT x holds
( W meets A & W meets A ` ) by Th20;
hence x in A ^Fodelta ; ::_thesis: verum
end;
hence A ^Fodelta = (A ^Fob) /\ ((A `) ^Fob) by SUBSET_1:3; ::_thesis: verum
end;
theorem :: FINTOPO2:40
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Fodelta = (A ^Fob) /\ ((A ^Foi) `)
proof
let FMT be non empty FMT_Space_Str ; ::_thesis: for A being Subset of FMT holds A ^Fodelta = (A ^Fob) /\ ((A ^Foi) `)
let A be Subset of FMT; ::_thesis: A ^Fodelta = (A ^Fob) /\ ((A ^Foi) `)
((A `) ^Fob) ` = A ^Foi by Th37;
hence A ^Fodelta = (A ^Fob) /\ ((A ^Foi) `) by Th39; ::_thesis: verum
end;
theorem :: FINTOPO2:41
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Fodelta = (A `) ^Fodelta
proof
let FMT be non empty FMT_Space_Str ; ::_thesis: for A being Subset of FMT holds A ^Fodelta = (A `) ^Fodelta
let A be Subset of FMT; ::_thesis: A ^Fodelta = (A `) ^Fodelta
A ^Fodelta = (((A `) `) ^Fob) /\ ((A `) ^Fob) by Th39;
hence A ^Fodelta = (A `) ^Fodelta by Th39; ::_thesis: verum
end;
theorem :: FINTOPO2:42
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Fodelta = (A ^Fob) \ (A ^Foi)
proof
let FMT be non empty FMT_Space_Str ; ::_thesis: for A being Subset of FMT holds A ^Fodelta = (A ^Fob) \ (A ^Foi)
let A be Subset of FMT; ::_thesis: A ^Fodelta = (A ^Fob) \ (A ^Foi)
for x being set holds
( x in A ^Fodelta iff x in (A ^Fob) \ (A ^Foi) )
proof
let x be set ; ::_thesis: ( x in A ^Fodelta iff x in (A ^Fob) \ (A ^Foi) )
thus ( x in A ^Fodelta implies x in (A ^Fob) \ (A ^Foi) ) ::_thesis: ( x in (A ^Fob) \ (A ^Foi) implies x in A ^Fodelta )
proof
assume x in A ^Fodelta ; ::_thesis: x in (A ^Fob) \ (A ^Foi)
then x in (A ^Fob) /\ ((((A `) ^Fob) `) `) by Th39;
then x in (A ^Fob) /\ ((A ^Foi) `) by Th37;
hence x in (A ^Fob) \ (A ^Foi) by SUBSET_1:13; ::_thesis: verum
end;
assume x in (A ^Fob) \ (A ^Foi) ; ::_thesis: x in A ^Fodelta
then x in (A ^Fob) /\ ((A ^Foi) `) by SUBSET_1:13;
then x in (A ^Fob) /\ ((((A `) ^Fob) `) `) by Th37;
hence x in A ^Fodelta by Th39; ::_thesis: verum
end;
hence A ^Fodelta = (A ^Fob) \ (A ^Foi) by TARSKI:1; ::_thesis: verum
end;
definition
let FMT be non empty FMT_Space_Str ;
let A be Subset of FMT;
funcA ^Fodel_i -> Subset of FMT equals :: FINTOPO2:def 14
A /\ (A ^Fodelta);
coherence
A /\ (A ^Fodelta) is Subset of FMT ;
funcA ^Fodel_o -> Subset of FMT equals :: FINTOPO2:def 15
(A `) /\ (A ^Fodelta);
coherence
(A `) /\ (A ^Fodelta) is Subset of FMT ;
end;
:: deftheorem defines ^Fodel_i FINTOPO2:def_14_:_
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Fodel_i = A /\ (A ^Fodelta);
:: deftheorem defines ^Fodel_o FINTOPO2:def_15_:_
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Fodel_o = (A `) /\ (A ^Fodelta);
theorem :: FINTOPO2:43
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Fodelta = (A ^Fodel_i) \/ (A ^Fodel_o)
proof
let FMT be non empty FMT_Space_Str ; ::_thesis: for A being Subset of FMT holds A ^Fodelta = (A ^Fodel_i) \/ (A ^Fodel_o)
let A be Subset of FMT; ::_thesis: A ^Fodelta = (A ^Fodel_i) \/ (A ^Fodel_o)
for x being set holds
( x in A ^Fodelta iff x in (A ^Fodel_i) \/ (A ^Fodel_o) )
proof
let x be set ; ::_thesis: ( x in A ^Fodelta iff x in (A ^Fodel_i) \/ (A ^Fodel_o) )
thus ( x in A ^Fodelta implies x in (A ^Fodel_i) \/ (A ^Fodel_o) ) ::_thesis: ( x in (A ^Fodel_i) \/ (A ^Fodel_o) implies x in A ^Fodelta )
proof
assume x in A ^Fodelta ; ::_thesis: x in (A ^Fodel_i) \/ (A ^Fodel_o)
then x in ([#] the carrier of FMT) /\ (A ^Fodelta) by XBOOLE_1:28;
then x in (A \/ (A `)) /\ (A ^Fodelta) by SUBSET_1:10;
hence x in (A ^Fodel_i) \/ (A ^Fodel_o) by XBOOLE_1:23; ::_thesis: verum
end;
assume x in (A ^Fodel_i) \/ (A ^Fodel_o) ; ::_thesis: x in A ^Fodelta
then x in (A \/ (A `)) /\ (A ^Fodelta) by XBOOLE_1:23;
then x in ([#] the carrier of FMT) /\ (A ^Fodelta) by SUBSET_1:10;
hence x in A ^Fodelta by XBOOLE_1:28; ::_thesis: verum
end;
hence A ^Fodelta = (A ^Fodel_i) \/ (A ^Fodel_o) by TARSKI:1; ::_thesis: verum
end;
definition
let FMT be non empty FMT_Space_Str ;
let G be Subset of FMT;
attrG is Fo_open means :Def16: :: FINTOPO2:def 16
G = G ^Foi ;
attrG is Fo_closed means :Def17: :: FINTOPO2:def 17
G = G ^Fob ;
end;
:: deftheorem Def16 defines Fo_open FINTOPO2:def_16_:_
for FMT being non empty FMT_Space_Str
for G being Subset of FMT holds
( G is Fo_open iff G = G ^Foi );
:: deftheorem Def17 defines Fo_closed FINTOPO2:def_17_:_
for FMT being non empty FMT_Space_Str
for G being Subset of FMT holds
( G is Fo_closed iff G = G ^Fob );
theorem :: FINTOPO2:44
for FMT being non empty FMT_Space_Str
for A being Subset of FMT st A ` is Fo_open holds
A is Fo_closed
proof
let FMT be non empty FMT_Space_Str ; ::_thesis: for A being Subset of FMT st A ` is Fo_open holds
A is Fo_closed
let A be Subset of FMT; ::_thesis: ( A ` is Fo_open implies A is Fo_closed )
assume A ` is Fo_open ; ::_thesis: A is Fo_closed
then A1: A ` = (A `) ^Foi by Def16;
(((A `) ^Foi) `) ` = (A ^Fob) ` by Th38;
hence A is Fo_closed by A1, Def17; ::_thesis: verum
end;
theorem :: FINTOPO2:45
for FMT being non empty FMT_Space_Str
for A being Subset of FMT st A ` is Fo_closed holds
A is Fo_open
proof
let FMT be non empty FMT_Space_Str ; ::_thesis: for A being Subset of FMT st A ` is Fo_closed holds
A is Fo_open
let A be Subset of FMT; ::_thesis: ( A ` is Fo_closed implies A is Fo_open )
assume A ` is Fo_closed ; ::_thesis: A is Fo_open
then A1: A ` = (A `) ^Fob by Def17;
(A `) ^Fob = (((A `) `) ^Foi) ` by Th38
.= (A ^Foi) ` ;
then A = ((A ^Foi) `) ` by A1
.= A ^Foi ;
hence A is Fo_open by Def16; ::_thesis: verum
end;
theorem :: FINTOPO2:46
for FMT being non empty FMT_Space_Str
for A, B being Subset of FMT st FMT is Fo_filled & ( for x being Element of FMT holds {x} in U_FMT x ) holds
(A /\ B) ^Fob = (A ^Fob) /\ (B ^Fob)
proof
let FMT be non empty FMT_Space_Str ; ::_thesis: for A, B being Subset of FMT st FMT is Fo_filled & ( for x being Element of FMT holds {x} in U_FMT x ) holds
(A /\ B) ^Fob = (A ^Fob) /\ (B ^Fob)
let A, B be Subset of FMT; ::_thesis: ( FMT is Fo_filled & ( for x being Element of FMT holds {x} in U_FMT x ) implies (A /\ B) ^Fob = (A ^Fob) /\ (B ^Fob) )
assume A1: FMT is Fo_filled ; ::_thesis: ( ex x being Element of FMT st not {x} in U_FMT x or (A /\ B) ^Fob = (A ^Fob) /\ (B ^Fob) )
assume A2: for x being Element of FMT holds {x} in U_FMT x ; ::_thesis: (A /\ B) ^Fob = (A ^Fob) /\ (B ^Fob)
A3: for C being Subset of FMT holds C ^Fob c= C
proof
let C be Subset of FMT; ::_thesis: C ^Fob c= C
for y being Element of FMT st y in C ^Fob holds
y in C
proof
let y be Element of FMT; ::_thesis: ( y in C ^Fob implies y in C )
assume A4: y in C ^Fob ; ::_thesis: y in C
{y} in U_FMT y by A2;
then {y} meets C by A4, Th20;
then ex z being set st
( z in {y} & z in C ) by XBOOLE_0:3;
hence y in C by TARSKI:def_1; ::_thesis: verum
end;
hence C ^Fob c= C by SUBSET_1:2; ::_thesis: verum
end;
A5: for C being Subset of FMT holds C ^Fob = C
proof
let C be Subset of FMT; ::_thesis: C ^Fob = C
( C c= C ^Fob & C ^Fob c= C ) by A1, A3, Th35;
hence C ^Fob = C by XBOOLE_0:def_10; ::_thesis: verum
end;
then ( (A /\ B) ^Fob = A /\ B & A ^Fob = A ) ;
hence (A /\ B) ^Fob = (A ^Fob) /\ (B ^Fob) by A5; ::_thesis: verum
end;
theorem :: FINTOPO2:47
for FMT being non empty FMT_Space_Str
for A, B being Subset of FMT st FMT is Fo_filled & ( for x being Element of FMT holds {x} in U_FMT x ) holds
(A ^Foi) \/ (B ^Foi) = (A \/ B) ^Foi
proof
let FMT be non empty FMT_Space_Str ; ::_thesis: for A, B being Subset of FMT st FMT is Fo_filled & ( for x being Element of FMT holds {x} in U_FMT x ) holds
(A ^Foi) \/ (B ^Foi) = (A \/ B) ^Foi
let A, B be Subset of FMT; ::_thesis: ( FMT is Fo_filled & ( for x being Element of FMT holds {x} in U_FMT x ) implies (A ^Foi) \/ (B ^Foi) = (A \/ B) ^Foi )
assume A1: FMT is Fo_filled ; ::_thesis: ( ex x being Element of FMT st not {x} in U_FMT x or (A ^Foi) \/ (B ^Foi) = (A \/ B) ^Foi )
assume A2: for x being Element of FMT holds {x} in U_FMT x ; ::_thesis: (A ^Foi) \/ (B ^Foi) = (A \/ B) ^Foi
A3: for C being Subset of FMT holds C c= C ^Foi
proof
let C be Subset of FMT; ::_thesis: C c= C ^Foi
for y being Element of FMT st y in C holds
y in C ^Foi
proof
let y be Element of FMT; ::_thesis: ( y in C implies y in C ^Foi )
assume y in C ; ::_thesis: y in C ^Foi
then A4: {y} is Subset of C by SUBSET_1:41;
{y} in U_FMT y by A2;
hence y in C ^Foi by A4; ::_thesis: verum
end;
hence C c= C ^Foi by SUBSET_1:2; ::_thesis: verum
end;
A5: for C being Subset of FMT holds C = C ^Foi
proof
let C be Subset of FMT; ::_thesis: C = C ^Foi
( C c= C ^Foi & C ^Foi c= C ) by A1, A3, Th36;
hence C = C ^Foi by XBOOLE_0:def_10; ::_thesis: verum
end;
then ( (A \/ B) ^Foi = A \/ B & A ^Foi = A ) ;
hence (A ^Foi) \/ (B ^Foi) = (A \/ B) ^Foi by A5; ::_thesis: verum
end;