:: Topology from Neighbourhoods
:: by Roland Coghetto
::
:: Received August 14, 2015
:: Copyright (c) 2015-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FINSET_1, CARD_1, XBOOLE_0, SUBSET_1, SETFAM_1, TARSKI, ZFMISC_1,
FUNCT_1, RELAT_1, FUNCOP_1, CARD_FIL, PCOMPS_1, STRUCT_0, ORDERS_2,
YELLOW_1, CONNSP_2, YELLOW_6, NAT_1, ARYTM_3, PARTFUN1, PRE_TOPC,
FINTOPO2, RCOMP_1, RLVECT_3, CANTOR_1, FILTER_0, XXREAL_1, YELLOW19,
CARDFIL2, FINTOPO7;
notations TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1,
ORDINAL1, SETFAM_1, FINSET_1, CARD_1,
RELSET_1, CARD_FIL, STRUCT_0, DOMAIN_1, NUMBERS, ORDERS_2, YELLOW_1,
NAT_1, CANTOR_1, FUNCT_2, FUNCOP_1, PARTFUN1, FINTOPO2, PRE_TOPC,
CONNSP_2, CARDFIL2;
constructors FINTOPO2, CANTOR_1, NAT_LAT, NAT_1, BORSUK_1, CARDFIL2, XXREAL_2,
SIMPLEX0;
registrations XBOOLE_0, SUBSET_1, RELSET_1, CARD_1, STRUCT_0, MEMBERED,
FUNCT_2, ZFMISC_1, FINTOPO2, PRE_TOPC;
requirements NUMERALS, SUBSET, BOOLE;
definitions TARSKI, XBOOLE_0;
equalities FUNCOP_1, FINTOPO2;
expansions TARSKI, XBOOLE_0, SETFAM_1, FINTOPO2, FUNCT_2, PRE_TOPC, CARDFIL2;
theorems TARSKI, FUNCT_1, FUNCT_2, SETFAM_1, ZFMISC_1, RELAT_1, XBOOLE_0,
XBOOLE_1, CARD_FIL, WAYBEL_7, FINTOPO2, PRE_TOPC, CONNSP_2, CANTOR_1,
YELLOW_9, SUBSET_1, PRE_CIRC, CARDFIL2;
schemes FUNCT_2, NAT_1;
begin :: Preliminaries
reserve X for non empty set;
theorem
for B,Y being Subset-Family of X st Y c= UniCl B holds union Y in UniCl B
proof
let B,Y be Subset-Family of X;
assume Y c= UniCl B;
then union Y in UniCl UniCl B by CANTOR_1:def 1;
hence thesis by YELLOW_9:15;
end;
theorem Th1:
for B being empty Subset-Family of X st (for B1,B2 being Element of B holds
ex BB being Subset of B st B1 /\ B2 = union BB) & X = union B
holds FinMeetCl B c= UniCl B
proof
let B be empty Subset-Family of X;
assume that
for B1,B2 be Element of B
ex BB being Subset of B st B1/\B2=union BB and
A1: X = union B;
FinMeetCl B c= UniCl B
proof
let x be object;
assume
A2: x in FinMeetCl B;
then reconsider x1=x as Subset of X;
consider Y be Subset-Family of X such that
A3: Y c= B and
Y is finite and
A4: x1=Intersect Y by A2,CANTOR_1:def 3;
Y={} & meet {}={} by A3,SETFAM_1:1;
then x1=X by A4,SETFAM_1:def 9;
hence x in UniCl B by A1,CANTOR_1:def 1;
end;
hence FinMeetCl B c= UniCl B;
end;
theorem Th2:
for B being non empty Subset-Family of X st
(for B1,B2 being Element of B holds
ex BB being Subset of B st B1/\B2 = union BB) & X = union B
holds FinMeetCl B c= UniCl B
proof
let B be non empty Subset-Family of X;
assume that
A1: for B1,B2 be Element of B
ex BB being Subset of B st B1/\B2=union BB and
A2: X = union B;
let x be object;
assume
A3: x in FinMeetCl B;
then reconsider x0=x as Subset of X;
consider Y be Subset-Family of X such that
A4: Y c= B and
A5: Y is finite and
A6: x0 = Intersect Y by A3,CANTOR_1:def 3;
defpred PP[Nat] means
for Y be Subset-Family of X,x be Subset of X st
Y c= B & card Y=$1 & x = Intersect Y holds
x in UniCl B;
A7: PP[0]
proof
let Y be Subset-Family of X,x be Subset of X;
assume that
Y c= B and
A8: card Y=0 and
A9: x = Intersect Y;
Y={} by A8; then
A10: x = X by A9,SETFAM_1:def 9;
reconsider x0=x as set;
thus x in UniCl B by A2,A10,CANTOR_1:def 1;
end;
A11:
for k being Nat holds PP[k] implies PP[k+1]
proof
let k be Nat;
assume
A12: PP[k];
let Y be Subset-Family of X,x be Subset of X;
assume that
A13: Y c= B and
A14: card Y=k+1 and
A15: x = Intersect Y;
Y is finite set by A14;
then consider x1 be Element of Y,C being Subset of Y such that
A16: Y=C\/{x1} and
A17: card C = k by A14,PRE_CIRC:24;
A18: C c= B & card C=k by A13,A17;
B c= bool X;
then C c= bool X by A13;
then reconsider C0=C as Subset-Family of X;
per cases;
suppose
A19: C = {};
meet {x1}=x1 by SETFAM_1:10; then
A20: Intersect Y = x1 by A19,A16,SETFAM_1:def 9;
then x1 in bool X;
then {x1} c= bool X by TARSKI:def 1;
then reconsider B0={x1} as Subset-Family of X;
x1 in Y by A16; then
A21: {x1} c= Y & Y c= B by A13,TARSKI:def 1;
x in B & B0 c= B & x=union B0 by A16,A21,A15,A20;
hence x in UniCl B by CANTOR_1:def 1;
end;
suppose
A22: C<>{};
then meet(C\/{x1})=meet(C) /\ meet({x1}) by SETFAM_1:9; then
A23: meet(Y)=meet C /\ x1 by A16,SETFAM_1:10;
meet Y =Intersect(Y) by A16,SETFAM_1:def 9; then
A24: Intersect(Y)=Intersect(C0)/\x1 by A22,A23,SETFAM_1:def 9;
Intersect(Y) in UniCl B
proof
Intersect(C0) in UniCl B by A18,A12;
then consider Y2 be Subset-Family of X such that
A25: Y2 c= B and
A26: Intersect(C0)=union Y2 by CANTOR_1:def 1;
per cases;
suppose
A27: Y2 is empty;
{} c= X;
then reconsider x0={} as Subset of X;
A28: {} c= bool X & {} c= B & {}=union {} by ZFMISC_1:2;
then reconsider S={} as Subset-Family of X;
thus thesis by A27,A24,A26,A28,CANTOR_1:def 1;
end;
suppose
A29: Y2 is non empty;
set Y3=the set of all y/\x1 where y is Element of Y2;
Y3 c= bool X
proof
let x be object;
assume
A30: x in Y3;
then reconsider x as Element of Y3;
consider y be Element of Y2 such that
A31: x=y/\x1 by A30;
A32: x c= x1 by A31,XBOOLE_1:17;
x1 in Y & Y c= bool X by A16;
then x1 c= X;
then x c= X by A32;
hence thesis;
end;
then reconsider Y3 as Subset-Family of X;
A33: union Y3=(union Y2) /\ x1
proof
hereby let x be object;
assume
A34: x in union Y3;
consider a1 be set such that
A35: x in a1 and
A36: a1 in Y3 by A34,TARSKI:def 4;
consider x2 be Element of Y2 such that
A37: a1=x2/\x1 by A36;
x in a1 & a1 c= x2 & a1 c= x1 by A35,A37,XBOOLE_1:17;
then x in union Y2 & x in x1 by A29,TARSKI:def 4;
hence x in (union Y2)/\x1 by XBOOLE_0:def 4;
end;
let x be object;
assume x in (union Y2)/\ x1; then
A38: x in union Y2 & x in x1 by XBOOLE_0:def 4;
then consider a be set such that
A39: x in a and
A40: a in Y2 by TARSKI:def 4;
reconsider a as Element of Y2 by A40;
A41: x in a/\x1 by A38,A39,XBOOLE_0:def 4;
a/\x1 in Y3;
hence x in union Y3 by A41,TARSKI:def 4;
end;
A42: Intersect(Y)=union Y3
proof
hereby let t be object;
assume t in Intersect(Y); then
A43: t in union Y2 & t in x1 by A24,A26,XBOOLE_0:def 4;
then consider t0 be set such that
A44: t in t0 and
A45: t0 in Y2 by TARSKI:def 4;
A46: t in t0/\x1 by A43,A44,XBOOLE_0:def 4;
t0/\x1 in Y3 by A45;
hence t in union Y3 by A46,TARSKI:def 4;
end;
let t be object;
assume t in union Y3;
then t in union Y2 & t in x1 by A33,XBOOLE_0:def 4;
then t in meet C0 & t in x1 by A26,A22,SETFAM_1:def 9;
then t in meet(C0) /\ x1 by XBOOLE_0:def 4;
hence t in Intersect Y by A23,A16,SETFAM_1:def 9;
end;
Y3 c= UniCl B
proof
let t be object;
assume t in Y3;
then consider a be Element of Y2 such that
A47: t=a/\x1;
reconsider a2=a as Element of B by A29,A25;
reconsider x2=x1 as Element of B by A13,A16;
consider BP being Subset of B such that
A48: a2/\x2 = union BP by A1;
reconsider ax=a2/\x2 as Subset of X;
BP c= B & B c= bool X; then
A49: BP c= bool X;
thus t in UniCl B by A47,A48,A49,CANTOR_1:def 1;
end;
then Intersect(Y) in UniCl UniCl B by A42,CANTOR_1:def 1;
hence thesis by YELLOW_9:15;
end;
end;
hence x in UniCl B by A15;
end;
end;
A50: for k being Nat holds PP[k] from NAT_1:sch 2(A7,A11);
reconsider CY=card Y as Nat by A5;
PP[CY] by A50;
hence x in UniCl B by A4,A6;
end;
theorem Th3:
for B being Subset-Family of X st (for B1,B2 being Element of B holds
ex BB being Subset of B st B1 /\ B2 = union BB) & X = union B
holds UniCl B = UniCl FinMeetCl B & TopStruct(#X,UniCl B#) is TopSpace-like
proof
let B be Subset-Family of X;
assume that
A1: (for B1,B2 be Element of B
ex BB being Subset of B st B1/\B2=union BB) and
A2: X = union B;
thus UniCl B=UniCl FinMeetCl B
proof
hereby let x be object;
assume
A3: x in UniCl B;
then reconsider x0=x as Subset of X;
consider Y being Subset-Family of X such that
A4: Y c= B and
A5: x=union Y by A3,CANTOR_1:def 1;
B c= FinMeetCl B by CANTOR_1:4;
then Y c= FinMeetCl B by A4;
hence x in UniCl FinMeetCl B by A5,CANTOR_1:def 1;
end;
let x be object;assume
A6: x in UniCl FinMeetCl B;
then reconsider x0=x as Subset of X;
consider Y1 being Subset-Family of X such that
A7: Y1 c= FinMeetCl B and
A8: x=union Y1 by A6,CANTOR_1:def 1;
FinMeetCl B c= UniCl B
proof
per cases;
suppose B is empty;
hence thesis by A1,A2,Th1;
end;
suppose B is non empty;
hence thesis by A1,A2,Th2;
end;
end;
then Y1 c= UniCl B by A7;
then union Y1 in UniCl UniCl B by CANTOR_1:def 1;
hence x in UniCl B by A8,YELLOW_9:15;
end;
hence TopStruct(#X,UniCl B#) is TopSpace-like by CANTOR_1:15;
end;
theorem
for FMT being non empty FMT_Space_Str holds ex S being RelStr st
for x being Element of FMT holds U_FMT x is Subset of S
proof
let FMT be non empty FMT_Space_Str;
set S=BoolePoset(the carrier of FMT);
take S;
thus thesis by WAYBEL_7:2;
end;
registration
let T be non empty TopSpace;
cluster NeighSp T -> Fo_filled;
coherence
proof
set NT=NeighSp T;
for x being Element of NT, D being Subset of NT st
D in U_FMT x holds x in D
proof
let x be Element of NT,D be Subset of NT such that
A1: D in U_FMT x;
U_FMT x = {V where V is Subset of T:
V in the topology of T & x in V} by FINTOPO2:def 7;
then consider V0 be Subset of T such that
A2: D=V0 and
V0 in the topology of T and
A3: x in V0 by A1;
thus thesis by A2,A3;
end;
hence thesis;
end;
end;
begin :: Open and Neighborhood in FMT_Space_Str
definition
let ET be non empty strict FMT_Space_Str, O be Subset of ET;
attr O is open means
:Def1:
for x being Element of ET st x in O holds O in U_FMT x;
end;
definition
let ET being non empty strict FMT_Space_Str;
attr ET is U_FMT_filter means
:Def2:
for x being Element of ET holds U_FMT x is Filter of the carrier of ET;
attr ET is U_FMT_with_point means
:Def3:
for x being Element of ET, V being Element of U_FMT x holds x in V;
attr ET is U_FMT_local means
:Def4:
for x being Element of ET,V being Element of U_FMT x
ex W being Element of U_FMT x st for y being Element of ET st
y is Element of W holds V is Element of U_FMT y;
end;
theorem Th4:
for ET being non empty strict FMT_Space_Str st ET is U_FMT_filter holds
for x being Element of ET holds U_FMT x is non empty;
theorem
for ET being non empty strict FMT_Space_Str st ET is U_FMT_with_point
holds ET is Fo_filled;
theorem Th5:
for ET being non empty strict FMT_Space_Str st ET is Fo_filled &
for x being Element of ET holds U_FMT x is non empty holds
ET is U_FMT_with_point
proof
let ET be non empty strict FMT_Space_Str such that
A1: ET is Fo_filled and
A2: for x be Element of ET holds U_FMT x is non empty;
for x be Element of ET, V be Element of U_FMT x holds x in V
proof
let x be Element of ET,V be Element of U_FMT x;
U_FMT x is non empty by A2;
then V in U_FMT x;
hence thesis by A1;
end;
hence thesis;
end;
theorem
for ET being non empty strict FMT_Space_Str st ET is Fo_filled &
ET is U_FMT_filter holds ET is U_FMT_with_point
proof
let ET be non empty strict FMT_Space_Str such that
A1: ET is Fo_filled and
A2: ET is U_FMT_filter;
for x be Element of ET holds U_FMT x is non empty by A2;
hence thesis by A1,Th5;
end;
registration
cluster U_FMT_local U_FMT_with_point U_FMT_filter for non empty
strict FMT_Space_Str;
existence
proof
set X = {{}},f = X --> {X};
A1: {{X}} c= bool bool X
proof
{X} c= bool X
proof
let x be object;
assume x in {X}; then
A2: x=X by TARSKI:def 1;
X c= X;
hence thesis by A2;
end;
then {X} in bool bool X;
hence thesis by TARSKI:def 1;
end;
A3: dom f = X & rng f={{X}} by RELAT_1:160;
reconsider f as PartFunc of X,bool bool X by A1,A3,FUNCT_2:2;
reconsider f as Function of X,bool bool X;
reconsider FMT=FMT_Space_Str(#X,f#) as non empty strict FMT_Space_Str;
A4: for x be Element of FMT holds U_FMT x = {X}
proof
let x be Element of FMT;
(the BNbd of FMT).x in {{X}} by FUNCT_2:5;
hence thesis by TARSKI:def 1;
end;
FMT is U_FMT_local & FMT is U_FMT_with_point & FMT is U_FMT_filter
proof
A5: now
let x be Element of FMT,
V be Element of U_FMT x;
U_FMT x is non empty by A4;
then V in U_FMT x;
then V in {X} by A4;
then V = X by TARSKI:def 1;
hence x in V;
end;
A6: for x be Element of FMT holds
U_FMT x is Filter of (the carrier of FMT)
proof
let x be Element of FMT;
reconsider Z={X} as Filter of X by CARD_FIL:4;
the carrier of FMT=X & Z={X} & Z is Filter of X;
hence thesis by A4;
end;
for x be Element of FMT,V be Element of U_FMT x ex
W be Element of U_FMT x st
for y be Element of FMT st y is Element of W holds
V is Element of U_FMT y
proof
let x be Element of FMT,V be Element of U_FMT x;
A7: V is Element of {X} by A4;
take X;
thus thesis by A7,A4,TARSKI:def 1;
end;
hence thesis by A5,A6;
end;
hence thesis;
end;
end;
theorem Th6:
for ET being U_FMT_filter non empty strict FMT_Space_Str,
x being Element of ET holds the carrier of ET in U_FMT x
proof
let ET be U_FMT_filter non empty strict FMT_Space_Str,
x be Element of ET;
U_FMT x is Filter of the carrier of ET by Def2;
hence thesis by CARD_FIL:5;
end;
definition
let ET being U_FMT_filter non empty strict FMT_Space_Str;
let x being Element of ET;
mode a_neighborhood of x -> Subset of ET means
:Def5:
it in U_FMT x;
existence
proof
the carrier of ET in U_FMT x by Th6;
hence thesis;
end;
end;
registration
let ET being U_FMT_filter non empty strict FMT_Space_Str;
let x being Element of ET;
cluster open for a_neighborhood of x;
existence
proof
set S = the carrier of ET;
take S;
A1: S in U_FMT x by Th6;
then reconsider S as Subset of ET;
S is open by Th6;
hence thesis by A1,Def5;
end;
end;
definition
let ET being U_FMT_filter non empty strict FMT_Space_Str;
let A being Subset of ET;
mode a_neighborhood of A -> Subset of ET means
:Def6:
for x being Element of ET st x in A holds it in U_FMT x;
existence
proof
set S=the carrier of ET;
S c= the carrier of ET;
then reconsider S as Subset of the carrier of ET;
take S;
hereby
let x be Element of ET such that x in A;
U_FMT x is Filter of the carrier of ET by Def2;
hence S in U_FMT x by CARD_FIL:5;
end;
end;
end;
registration
let ET being U_FMT_filter non empty strict FMT_Space_Str;
let A being Subset of ET;
cluster open for a_neighborhood of A;
existence
proof
set S=the carrier of ET;
S c= the carrier of ET;
then reconsider S as Subset of ET;
for x be Element of ET st x in A holds S in U_FMT x by Th6; then
A1: S is a_neighborhood of A by Def6;
S is open by Th6;
hence thesis by A1;
end;
end;
theorem Th7:
for ET being U_FMT_filter non empty strict FMT_Space_Str,
A being Subset of ET holds for NA being a_neighborhood of A,
B being Subset of ET st NA c= B holds B is a_neighborhood of A
proof
let ET be U_FMT_filter non empty strict FMT_Space_Str,A be Subset of ET;
let NA be a_neighborhood of A,B be Subset of ET;
assume
A1: NA c= B;
for x be Element of ET st x in A holds B in U_FMT x
proof
let x be Element of ET;
assume x in A; then
A2: NA in U_FMT x by Def6;
U_FMT x is Filter of the carrier of ET by Def2;
hence thesis by A1,A2,CARD_FIL:def 1;
end;
hence thesis by Def6;
end;
definition
let ET being U_FMT_filter non empty strict FMT_Space_Str;
let A being Subset of ET;
func Neighborhood A -> Subset-Family of ET equals
the set of all N where N is a_neighborhood of A;
correctness
proof
the set of all N where N is a_neighborhood of A is
Subset-Family of the carrier of ET
proof
the set of all N where N is a_neighborhood of A
c= bool the carrier of ET
proof
let t be object;
assume t in the set of all N where N is a_neighborhood of A;
then consider N0 be a_neighborhood of A such that
A1: t=N0;
thus thesis by A1;
end;
hence thesis;
end;
hence thesis;
end;
end;
theorem Th7bis:
for ET being U_FMT_filter non empty strict FMT_Space_Str,
A being non empty Subset of ET holds
Neighborhood A is Filter of the carrier of ET
proof
let ET be U_FMT_filter non empty strict FMT_Space_Str,
A be non empty Subset of ET;
set S=the set of all F where F is a_neighborhood of A;
S is Filter of the carrier of ET
proof
A1: S is non empty Subset-Family of the carrier of ET
proof
A2: S is non empty
proof
set Sq=the carrier of ET;
Sq c= the carrier of ET;
then reconsider Sq as Subset of the carrier of ET;
Sq is a_neighborhood of A
proof
for x be Element of ET st x in A holds Sq in U_FMT x by Th6;
hence thesis by Def6;
end;
then Sq in S;
hence thesis;
end;
S is Subset-Family of the carrier of ET
proof
S c= bool the carrier of ET
proof
let t be object;
assume t in S;
then consider F0 be a_neighborhood of A such that
A3: t=F0;
thus t in bool the carrier of ET by A3;
end;
hence thesis;
end;
hence thesis by A2;
end;
A4: not {} in S
proof
assume {} in S;
then consider F0 be a_neighborhood of A such that
A5: {}=F0;
A is non empty;
then consider a be object such that
A6: a in A;
reconsider a0=a as Element of ET by A6;
A7: {} in U_FMT a0 by A5,A6,Def6;
U_FMT a0 is Filter of the carrier of ET by Def2;
hence thesis by A7,CARD_FIL:def 1;
end;
for Y1,Y2 being Subset of ET holds
(Y1 in S & Y2 in S implies Y1/\Y2 in S) &
(Y1 in S & Y1 c= Y2 implies Y2 in S)
proof
let Y1,Y2 being Subset of ET;
now
assume that
A8: Y1 in S and
A9: Y2 in S;
consider F1 be a_neighborhood of A such that
A10: Y1=F1 by A8;
consider F2 be a_neighborhood of A such that
A11: Y2=F2 by A9;
A12: for x be Element of ET st x in A holds Y1/\Y2 in U_FMT x
proof
let x be Element of ET;
assume x in A; then
A13: Y1 in U_FMT x & Y2 in U_FMT x by A10,A11,Def6;
U_FMT x is Filter of the carrier of ET by Def2;
hence thesis by A13,CARD_FIL:def 1;
end;
Y1/\Y2 is a_neighborhood of A by A12,Def6;
hence Y1/\Y2 in S;
end;
hence Y1 in S & Y2 in S implies Y1/\Y2 in S;
now
assume that
A14: Y1 in S and
A15: Y1 c= Y2;
consider y1 be a_neighborhood of A such that
A16: y1=Y1 by A14;
for x be Element of ET st x in A holds Y2 in U_FMT x
proof
let x be Element of ET;
assume x in A; then
A17: Y1 in U_FMT x by A16,Def6;
U_FMT x is Filter of the carrier of ET by Def2;
hence thesis by A17,A15,CARD_FIL:def 1;
end;
then Y2 is a_neighborhood of A by Def6;
hence Y1 in S & Y1 c= Y2 implies Y2 in S;
end;
hence thesis;
end;
hence thesis by A1,A4,CARD_FIL:def 1;
end;
hence thesis;
end;
definition
let ET being non empty strict FMT_Space_Str;
attr ET is U_FMT_filter_base means
for x being Element of the carrier of ET holds
U_FMT x is filter_base of the carrier of ET;
end;
definition
let ET being non empty FMT_Space_Str;
func <.ET.] -> Function of the carrier of ET,
bool bool the carrier of ET means
:Def7:
for x be Element of the carrier of ET holds it.x=<.(U_FMT x).];
existence
proof
deffunc FF(Element of the carrier of ET)=<.(U_FMT $1).];
consider f being Function of the carrier of ET,
bool bool the carrier of ET
such that
A1: for x be Element of the carrier of ET holds f.x = FF(x)
from FUNCT_2:sch 4;
thus thesis by A1;
end;
uniqueness
proof
for Y1,Y2 be Function of the carrier of ET,bool bool the carrier of ET st
(for x be Element of the carrier of ET holds Y1.x=<.(U_FMT x).] &
for y be Element of the carrier of ET holds Y2.y=<.(U_FMT y).])
holds Y1=Y2
proof
let Y1,Y2 be Function of the carrier of ET,bool bool the carrier of ET
such that
A2: for x be Element of the carrier of ET holds
Y1.x=<.(U_FMT x).] &
for y be Element of the carrier of ET holds Y2.y=<.(U_FMT y).];
for t be object st t in the carrier of ET holds Y1.t=Y2.t
proof
let t be object such that
A3: t in the carrier of ET;
reconsider t as Element of the carrier of ET by A3;
Y1.t=<.(U_FMT t).] & Y2.t=<.(U_FMT t).] by A2;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
end;
definition
let ET being non empty strict FMT_Space_Str;
func gen_filter(ET) -> non empty strict FMT_Space_Str equals
FMT_Space_Str(#the carrier of ET,<.ET.] #);
correctness;
end;
theorem Th8:
for ET being non empty strict FMT_Space_Str st ET is U_FMT_filter_base
holds gen_filter(ET) is U_FMT_filter
proof
let ET be non empty strict FMT_Space_Str such that
A1: ET is U_FMT_filter_base;
for x be Element of gen_filter(ET)
holds U_FMT x is Filter of the carrier of gen_filter(ET)
proof
let x be Element of gen_filter(ET);
reconsider x0=x as Element of ET;
U_FMT x0 is filter_base of the carrier of ET by A1;
then <.U_FMT x0.] is Filter of the carrier of ET by CARDFIL2:25;
hence thesis by Def7;
end;
hence thesis;
end;
begin :: Topology from Neighbourhoods
definition
mode FMT_TopSpace is U_FMT_local
U_FMT_with_point U_FMT_filter non empty strict FMT_Space_Str;
end;
notation
let ET being FMT_TopSpace,x being Element of ET;
synonym NeighborhoodSystem x for U_FMT x;
end;
registration
let ET being FMT_TopSpace;
cluster open for Subset of ET;
existence
proof
A1: ET is U_FMT_filter;
set S=the carrier of ET;
S c= the carrier of ET;
then reconsider S=the carrier of ET as Subset of ET;
take S;
for x be Element of ET st x in S holds S in U_FMT x
proof
let x be Element of ET;
assume x in S;
U_FMT x is Filter of the carrier of ET by A1;
hence S in U_FMT x by CARD_FIL:5;
end;
hence thesis;
end;
end;
definition
let ET being FMT_TopSpace;
func Family_open_set(ET) -> non empty Subset-Family
of the carrier of ET equals
the set of all O where O is open Subset of ET;
correctness
proof
set OO = the set of all O where O is open Subset of ET;
A1: OO is non empty
proof
the carrier of ET is open Subset of ET
proof
A2: ET is U_FMT_filter;
set S=the carrier of ET;
S c= the carrier of ET;
then reconsider S as Subset of ET;
for x be Element of ET st x in S holds S in U_FMT x
proof
let x be Element of ET;
assume x in S;
U_FMT x is Filter of the carrier of ET by A2;
hence S in U_FMT x by CARD_FIL:5;
end;
hence thesis by Def1;
end;
then the carrier of ET in OO;
hence thesis;
end;
now
let t be object;
assume t in OO;
then consider OO1 be open Subset of ET such that
A3: t=OO1;
thus t in bool the carrier of ET by A3;
end;
then OO c= bool the carrier of ET;
hence thesis by A1;
end;
end;
theorem Th9:
for ET being FMT_TopSpace holds
{} in Family_open_set(ET) &
the carrier of ET in Family_open_set(ET) &
(for a being Subset-Family of ET st a c= Family_open_set(ET) holds
union a in Family_open_set(ET)) &
(for a, b being Subset of ET st a in Family_open_set(ET) &
b in Family_open_set(ET) holds a /\ b in Family_open_set(ET))
proof
let ET be FMT_TopSpace;
A1: ET is U_FMT_filter;
thus {} in Family_open_set(ET)
proof
set S={};
S c= the carrier of ET;
then reconsider S as Subset of ET;
S is open;
then reconsider S as open Subset of ET;
S in the set of all O where O is open Subset of ET;
hence thesis;
end;
thus the carrier of ET in Family_open_set(ET)
proof
set S=the carrier of ET;
S c= the carrier of ET;
then reconsider S as Subset of ET;
for x be Element of ET st x in S holds S in U_FMT x
proof
let x be Element of ET;
assume x in S;
U_FMT x is Filter of the carrier of ET by A1;
hence S in U_FMT x by CARD_FIL:5;
end;
then S is open;
then reconsider S as open Subset of ET;
S in the set of all O where O is open Subset of ET;
hence thesis;
end;
thus ( for a being Subset-Family of ET st a c= Family_open_set(ET) holds
union a in Family_open_set(ET) )
proof
let a being Subset-Family of ET such that
A2: a c= Family_open_set(ET);
reconsider UA=union a as Subset of ET;
now
let x be Element of ET;
assume x in UA;
then consider Y be set such that
A3: x in Y and
A4: Y in a by TARSKI:def 4;
Y in the set of all O where O is open Subset of ET by A2,A4;
then consider Y0 be open Subset of ET such that
A5: Y=Y0;
A6: Y in U_FMT x by A3,A5,Def1;
A7: Y c= UA by A4,ZFMISC_1:74;
U_FMT x is Filter of the carrier of ET by A1;
hence UA in U_FMT x by A6,A7,CARD_FIL:def 1;
end;
then UA is open;
hence thesis;
end;
thus for a, b being Subset of ET st a in Family_open_set(ET) &
b in Family_open_set(ET)
holds
a /\ b in Family_open_set(ET)
proof
let a,b being Subset of ET such that
A9: a in Family_open_set(ET) and
A10: b in Family_open_set(ET);
now
let x be Element of ET such that
A11: x in a/\b;
A12: x in a & x in b by A11,XBOOLE_0:def 4;
consider a0 be open Subset of ET such that
A13: a = a0 by A9;
A14: a in U_FMT x by A12,A13,Def1;
consider b0 be open Subset of ET such that
A15: b = b0 by A10;
A16: b in U_FMT x by A12,A15,Def1;
U_FMT x is Filter of the carrier of ET by A1;
hence a/\b in U_FMT x by A14,A16,CARD_FIL:def 1;
end;
then a/\b is open;
then reconsider AB=a/\b as open Subset of ET;
AB in the set of all O where O is open Subset of ET;
hence thesis;
end;
end;
theorem Th10:
for ET being FMT_TopSpace,a being Element of ET,
V being a_neighborhood of a holds
ex O being open Subset of ET st a in O & O c= V
proof
let ET be FMT_TopSpace,
a be Element of ET, V be a_neighborhood of a;
set O={x where x is Element of ET : V is a_neighborhood of x};
O is Subset of ET
proof
O c= the carrier of ET
proof
let x be object;
assume x in O;
then consider t be Element of ET such that
A1: x=t and
V is a_neighborhood of t;
thus thesis by A1;
end;
hence thesis;
end;
then reconsider O as Subset of ET;
A2: O is open Subset of ET
proof
for x be Element of ET st x in O holds O in U_FMT x
proof
let x be Element of ET;
assume x in O;
then consider t be Element of ET such that
A3: x=t and
A4: V is a_neighborhood of t;
x is Element of ET & V is Element of U_FMT x by A3,A4,Def5;
then consider W be Element of U_FMT x such that
A5: for y be Element of ET st y is Element of W holds
V is Element of U_FMT y by Def4;
A6: W c= O
proof
let v be object such that E1:v in W;
U_FMT x is non empty by Th4;
then W in U_FMT x;
then reconsider v as Element of ET by E1;
A7: v is Element of ET & V is Element of U_FMT v by E1,A5;
U_FMT v is non empty by Th4;
then V is a_neighborhood of v by A7,Def5;
hence thesis;
end;
W in U_FMT x & U_FMT x is Filter of the carrier of ET
proof
hereby
U_FMT x is non empty by Th4;
hence W in U_FMT x;
end;
thus U_FMT x is Filter of the carrier of ET by Def2;
end;
hence thesis by A6,CARD_FIL:def 1;
end;
hence thesis by Def1;
end;
A8: a in O;
O c= V
proof
let x be object;
assume x in O;
then consider x0 be Element of ET such that
A9: x=x0 and
A10: V is a_neighborhood of x0;
V in U_FMT x0 by A10,Def5;
hence x in V by A9,Def3;
end;
hence thesis by A2,A8;
end;
theorem Th11:
for ET being FMT_TopSpace, A being non empty Subset of ET holds
for V being Subset of ET holds V is a_neighborhood of A iff
ex O being open Subset of ET st A c= O & O c= V
proof
let ET be FMT_TopSpace,
A be non empty Subset of ET;
let V be Subset of ET;
thus V is a_neighborhood of A implies
ex O be open Subset of ET st A c= O & O c= V
proof
assume
A1: V is a_neighborhood of A;
A2: now
let a be Element of ET;
assume a in A;
then V in U_FMT a by A1,Def6;
then V is a_neighborhood of a by Def5;
hence ex O be open Subset of ET st a in O & O c= V by Th10;
end;
defpred P[object,object] means
ex x be Element of ET,y be open Subset of ET
st x=$1 & y=$2 &
x in y & y c= V;
A3: for x being object st x in A ex y being object st
y in bool the carrier of ET & P[x,y]
proof
let x being object such that
A4: x in A;
reconsider x as Element of A by A4;
consider O be open Subset of ET such that
A5: x in O and
A6: O c= V by A2;
thus thesis by A5,A6;
end;
ex f being Function of A,bool the carrier of ET st
for x being object st x in A holds P[x,f.x] from FUNCT_2:sch 1(A3);
then consider f being Function of A,bool the carrier of ET such that
A7: for x being object st x in A holds P[x,f.x];
set OO=union rng f;
OO is open Subset of ET & A c= OO & OO c= V
proof
reconsider OO as Subset of ET;
A8: OO is open Subset of ET & OO c= V
proof
A9: for a be Element of ET st a in A holds
f.a is open Subset of ET & f.a c= V
proof
let a be Element of ET;
assume a in A;
then P[a,f.a] by A7;
then consider x1 be set,y1 be open Subset of ET such that
a=x1 and
A10: f.a=y1 and
x1 in y1 and
A11: y1 c= V;
thus thesis by A11,A10;
end;
A12: OO c= V
proof
let t be object;
assume t in OO;
then consider T be set such that
A13: t in T and
A14: T in rng f by TARSKI:def 4;
consider x be object such that
A15: x in dom f and
A16: T=f.x by A14,FUNCT_1:def 3;
x in A by A15;
then f.x c= V by A9;
hence thesis by A13,A16;
end;
rng f c= Family_open_set(ET)
proof
let t be object;
assume t in rng f;
then consider x be object such that
A17: x in dom f and
A18: t=f.x by FUNCT_1:def 3;
A19: x in A by A17;
f.x is open Subset of ET by A19,A9;
hence thesis by A18;
end;
then union rng f in the set of all O where
O is open Subset of ET by Th9;
then consider O1 be open Subset of ET such that
A20: union rng f=O1;
thus thesis by A20,A12;
end;
A c= OO
proof
let t be object;
assume
A21: t in A;
then P[t,f.t] by A7;
then consider x1,y1 be set such that
A22: t=x1 and
A23: f.t=y1 and
A24: x1 in y1 and
y1 c= V;
y1 in rng f by A23,A21,FUNCT_2:4;
hence thesis by A22,A24,TARSKI:def 4;
end;
hence thesis by A8;
end;
hence thesis;
end;
thus (ex O be open Subset of ET st A c= O & O c= V) implies
V is a_neighborhood of A
proof
given O be open Subset of ET such that
A25: A c= O and
A26: O c= V;
for x be Element of ET st x in A holds O in U_FMT x by A25,Def1;
then O is a_neighborhood of A by Def6;
hence thesis by A26,Th7;
end;
end;
theorem
for ET being FMT_TopSpace, A being non empty Subset of ET
holds Neighborhood A is Filter of the carrier of ET by Th7bis;
definition
let ET being FMT_TopSpace, A being non empty Subset of ET;
func OpenNeighborhoods A -> Subset-Family of the carrier of ET equals
the set of all N where N is open a_neighborhood of A;
correctness
proof
the set of all N where N is
open a_neighborhood of A c= bool the carrier of ET
proof
let t be object;
assume t in the set of all N where N is open a_neighborhood of A;
then consider N be open a_neighborhood of A such that
A1: t=N;
thus thesis by A1;
end;
hence thesis;
end;
end;
theorem
for ET being FMT_TopSpace, cF being Filter of the carrier of ET,
cS being non empty Subset of cF holds for A being non empty Subset of ET
st cF = Neighborhood A & cS = OpenNeighborhoods A holds cS is filter_basis
proof
let ET be FMT_TopSpace,
cF be Filter of the carrier of ET,
cS be non empty Subset of cF;
let A be non empty Subset of ET
such that
A1: cF = Neighborhood A and
A2: cS = OpenNeighborhoods A;
for f be Element of cF holds ex b be Element of cS st b c= f
proof
let f be Element of cF;
f in the set of all N where N is a_neighborhood of A by A1;
then consider N be a_neighborhood of A such that
A3: f = N;
consider O be open Subset of ET such that
A4: A c= O & O c= N by Th11;
O is open;
then for x be Element of ET st x in A holds O in U_FMT x by A4;
then O is open a_neighborhood of A by Def6;
then O in the set of all N where N is open a_neighborhood of A;
hence thesis by A2,A3,A4;
end;
hence thesis;
end;
theorem Th12:
for T being non empty TopSpace holds ex ET being FMT_TopSpace st
the carrier of T = the carrier of ET &
Family_open_set(ET) = the topology of T
proof
let T be non empty TopSpace;
ex ET be non empty strict FMT_Space_Str st
ET is U_FMT_filter & ET is U_FMT_with_point & ET is U_FMT_local &
the carrier of T = the carrier of ET &
ex TT be FMT_TopSpace st
TT=ET & Family_open_set(TT)=the topology of T
proof
deffunc F(object)={O where O is Element of the topology of T: $1 in O};
A1: for x being object st x in the carrier of T holds
F(x) in bool bool the carrier of T
proof
let x being object such that
A2: x in the carrier of T;
reconsider x as Element of T by A2;
F(x) c= bool the carrier of T
proof
let t be object such that
A3: t in F(x);
consider O1 be Element of the topology of T such that
A4: t=O1 and
x in O1 by A3;
thus thesis by A4;
end;
hence thesis;
end;
ex f being Function of the carrier of T,bool bool the carrier of T st
for x being object st x in the carrier of T holds
f.x=F(x) from FUNCT_2:sch 2(A1);
then consider f be Function of
the carrier of T,bool bool the carrier of T
such that
A5: for x being object st x in the carrier of T holds f.x=F(x);
reconsider TMP=FMT_Space_Str(#the carrier of T,f#) as
non empty strict FMT_Space_Str;
A6: for t be Element of TMP holds U_FMT t is non empty
proof
let t be Element of TMP;
take TT=the carrier of T;
TT in the topology of T by PRE_TOPC:def 1;
then TT in F(t);
hence thesis by A5;
end;
A7: TMP is U_FMT_filter_base
proof
for x be Element of the carrier of TMP holds
U_FMT x is non empty &
U_FMT x is with_non-empty_elements &
for B1,B2 be Element of U_FMT x
ex B be Element of U_FMT x st B c= B1/\B2
proof
let x be Element of the carrier of TMP;
thus
A8: U_FMT x is non empty by A6;
thus U_FMT x is with_non-empty_elements
proof
assume that
A9: not (U_FMT x is with_non-empty_elements);
{} in F(x) by A9,A5;
then consider O be Element of the topology of T such that
A10: O={} and
A11: x in O;
thus thesis by A10,A11;
end;
thus for B1,B2 be Element of U_FMT x
ex B be Element of U_FMT x st B c= B1/\B2
proof
let B1,B2 be Element of U_FMT x;
B1 in U_FMT x & B2 in U_FMT x by A8; then
A12: B1 in F(x) & B2 in F(x) by A5;
then consider O1 be Element of the topology of T such that
A13: B1=O1 and
A14: x in O1;
consider O2 be Element of the topology of T such that
A15: B2=O2 and
A16: x in O2 by A12;
A17: x in O1/\O2 by A14,A16,XBOOLE_0:def 4;
reconsider OO=O1/\O2 as Element of the topology of T
by PRE_TOPC:def 1;
OO in F(x) by A17;
then reconsider OO as Element of U_FMT x by A5;
take OO;
thus thesis by A13,A15;
end;
end;
then for x be Element of the carrier of TMP holds
U_FMT x is non empty & U_FMT x is with_non-empty_elements &
U_FMT x is quasi_basis;
hence thesis;
end;
reconsider ET=gen_filter(TMP) as non empty strict FMT_Space_Str;
take ET;
thus ET is U_FMT_filter by A7,Th8;
thus
A18: ET is U_FMT_with_point
proof
for x be Element of ET, V be Element of U_FMT x holds x in V
proof
let x be Element of ET,V be Element of U_FMT x;
set Z=(the BNbd of gen_filter(TMP)).x;
reconsider x0=x as Element of TMP;
A20: U_FMT x=<.(U_FMT x0).] by Def7;
A21: U_FMT x0 = F(x0) by A5;
then reconsider FX0=F(x0) as Subset-Family of the carrier of TMP;
A22: V is Element of <.(FX0).] by A5,A20;
<.FX0.] is non empty
proof
the carrier of T in the topology of T by PRE_TOPC:def 1;
then the carrier of T in FX0;
then reconsider XX=the carrier of T as Element of FX0;
FX0 c= <.FX0.] by CARDFIL2:def 8;
hence thesis by A21,A6;
end;
then V in <.FX0.] by A22;
then consider b be Element of FX0 such that
A23: b c= V by CARDFIL2:def 8;
F(x0) is non empty
proof
the carrier of T in the topology of T by PRE_TOPC:def 1;
then the carrier of T in F(x0);
hence thesis;
end;
then b in F(x0);
then consider OO be Element of the topology of T such that
A24: b=OO and
A25: x0 in OO;
thus thesis by A23,A24,A25;
end;
hence thesis;
end;
thus
A26: ET is U_FMT_local
proof
for x be Element of ET holds
for V be Element of U_FMT x ex W be Element of U_FMT x st
for y be Element of ET st y is Element of W holds
V is Element of U_FMT y
proof
let t be Element of ET;
set Z=(the BNbd of gen_filter(TMP)).t;
reconsider t0=t as Element of TMP;
A28: U_FMT t=<.(U_FMT t0).] by Def7;
A29: U_FMT t0 = F(t0) by A5;
then reconsider FT0=F(t0) as Subset-Family of the carrier of TMP;
for V be Element of U_FMT t ex W be Element of U_FMT t st
for y be Element of ET st y is Element of W holds
V is Element of U_FMT y
proof
let V be Element of U_FMT t;
A30: <.FT0.] is non empty
proof
the carrier of T in the topology of T by PRE_TOPC:def 1;
then the carrier of T in FT0;
then reconsider XX=the carrier of T as Element of FT0;
XX in <.FT0.]
proof
XX is Element of FT0 & XX c= XX;
hence thesis by CARDFIL2:def 8;
end;
hence thesis;
end;
A31: V in <.FT0.] by A30,A28,A29;
consider V0 be Element of FT0 such that
A32: V0 c= V by A31,CARDFIL2:def 8;
A33: F(t0) is non empty
proof
the carrier of T in the topology of T by PRE_TOPC:def 1;
then the carrier of T in F(t0);
hence thesis;
end;
then V0 in F(t0);
then consider OUV be Element of the topology of T such that
A34: V0=OUV and
A35: t0 in OUV;
reconsider W=OUV as Element of U_FMT t
by A28,A29,A34,CARDFIL2:def 8;
take W;
for y be Element of ET st y is Element of W holds
V is Element of U_FMT y
proof
let y be Element of ET such that
A36: y is Element of W;
set Z=(the BNbd of gen_filter(TMP)).y;
reconsider y0=y as Element of TMP;
A38: U_FMT y0 = F(y0) by A5;
then reconsider FY0=F(y0) as Subset-Family of the carrier of TMP;
A39: V0 in F(y0) by A34,A36,A35;
V0 in FT0 & FT0 c= bool the carrier of TMP by A33;
then reconsider VV0=V0 as Subset of the carrier of TMP;
V in <.FY0.] by A39,A32,A31,CARDFIL2:def 8;
hence thesis by Def7,A38;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
thus the carrier of T = the carrier of ET;
ex TT be FMT_TopSpace st TT=ET & Family_open_set(TT)=the topology of T
proof
reconsider TT=ET as FMT_TopSpace
by A7,Th8,A18,A26;
Family_open_set(TT)=the topology of T
proof
A41: Family_open_set(TT) c= the topology of T
proof
for t be object st t in Family_open_set(TT) holds
t in the topology of T
proof
let t be object;
assume t in Family_open_set(TT);
then consider O be open Subset of TT such that
A42: t=O;
per cases;
suppose O is empty;
hence thesis by A42,PRE_TOPC:1;
end;
suppose not O is empty;
reconsider O as Subset of T;
A44: for x be Point of T st x in O ex b being Subset of T
st b is a_neighborhood of x & b c= O
proof
let x be Point of T;
assume
A45: x in O;
reconsider x0=x as Element of ET;
A46: O in U_FMT x0 by A45,Def1;
set Z=(the BNbd of gen_filter(TMP)).x0;
reconsider x1=x0 as Element of TMP;
O in <.(U_FMT x1).] by A46,Def7;
then consider b be Element of U_FMT x1 such that
A48: b c= O by CARDFIL2:def 8;
U_FMT x1 is non empty & b is Element of U_FMT x1 by A6;
then b in U_FMT x1;
then b in F(x1) by A5;
then consider b0 be Element of the topology of T such that
A49: b=b0 and
A50: x1 in b0;
b0 is open;
hence thesis by A48,A49,A50,CONNSP_2:3;
end;
thus thesis by A44,CONNSP_2:7,A42,PRE_TOPC:def 2;
end;
end;
hence thesis;
end;
the topology of T c= Family_open_set(TT)
proof
let t be object;
assume
A51: t in the topology of T;
then reconsider t as Subset of TT;
t is open
proof
for x be Element of ET st x in t holds t in U_FMT x
proof
let x be Element of ET;
assume
A53: x in t;
set Z=(the BNbd of gen_filter(TMP)).x;
reconsider x0=x as Element of TMP;
A55: U_FMT x=<.(U_FMT x0).] by Def7;
U_FMT x0 = F(x0) by A5;
then reconsider FX0=F(x0) as
Subset-Family of the carrier of TMP;
t in F(x0) by A51,A53;
then t in U_FMT x0 by A5;
hence thesis by A55,CARDFIL2:def 8;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis by A41;
end;
hence thesis;
end;
hence thesis;
end;
then consider ET be non empty strict FMT_Space_Str such that
A56:the carrier of T = the carrier of ET and
ET is U_FMT_filter & ET is U_FMT_with_point & ET is U_FMT_local and
A57:ex TT be FMT_TopSpace st
TT=ET & Family_open_set(TT)=the topology of T;
consider TT be FMT_TopSpace such that
A58:TT=ET and
Family_open_set(TT)=the topology of T by A57;
take TT;
thus thesis by A56,A57,A58;
end;
theorem Th13:
for T being non empty TopSpace, ET being FMT_TopSpace st
the carrier of T = the carrier of ET &
Family_open_set(ET) = the topology of T holds
for x being Element of ET holds
U_FMT x = {V where V is Subset of ET:
ex O being Subset of T st O in the topology of T & x in O & O c= V}
proof
let T be non empty TopSpace,
ET be FMT_TopSpace;
assume that
the carrier of T = the carrier of ET and
A1: Family_open_set(ET)=the topology of T;
A2: for o be set st o in Family_open_set(ET) holds
for x be Element of ET st x in o holds o in U_FMT x
proof
let o be set;
assume o in Family_open_set(ET);
then consider O be open Subset of ET such that
A3: o=O;
thus thesis by A3,Def1;
end;
for x be Element of ET holds
U_FMT x = {V where V is Subset of ET:
ex O be Subset of T st O in the topology of T & x in O & O c= V}
proof
let x be Element of ET;
A4: U_FMT x c= {V where V is Subset of ET:
ex O be Subset of T st O in the topology of T & x in O & O c= V}
proof
let t be object;
assume
A5: t in U_FMT x; then
A6: t is a_neighborhood of x by Def5;
reconsider t as Subset of ET by A5;
consider OO be open Subset of ET such that
A7: x in OO and
A8: OO c= t by A6,Th10;
A9: OO in Family_open_set(ET);
then reconsider OO as Subset of T by A1;
thus thesis by A7,A8,A9,A1;
end;
{V where V is Subset of ET:
ex O be Subset of T st O in the topology of T & x in O & O c= V} c=
U_FMT x
proof
let t be object;
assume t in {V where V is Subset of ET:
ex O be Subset of T st O in the topology of T & x in O & O c= V};
then consider V be Subset of ET such that
A10: t=V and
A11: ex O be Subset of T st O in the topology of T & x in O & O c= V;
consider O2 be Subset of T such that
A12: O2 in the topology of T and
A13: x in O2 and
A14: O2 c= V by A11;
A15: O2 in U_FMT x by A12,A1,A2,A13;
U_FMT x is Filter of the carrier of ET by Def2;
hence thesis by A14,CARD_FIL:def 1,A15,A10;
end;
hence thesis by A4;
end;
hence thesis;
end;
begin :: Basis
definition
let ET being FMT_TopSpace, F being Subset-Family of ET;
attr F is quasi_basis means
:Def8:
Family_open_set(ET) c= UniCl F;
end;
registration
let ET being FMT_TopSpace;
cluster Family_open_set(ET) -> quasi_basis;
coherence
proof
reconsider F=Family_open_set ET as Subset-Family of ET;
let x be object;
assume
A1: x in Family_open_set ET;
then reconsider B={x} as Subset-Family of ET by SUBSET_1:41;
A2: B c= Family_open_set ET by A1,ZFMISC_1:31;
x=union B;
hence thesis by A2,CANTOR_1:def 1;
end;
end;
registration
let ET being FMT_TopSpace;
cluster quasi_basis for Subset-Family of ET;
existence
proof
reconsider OP=Family_open_set(ET) as Subset-Family of ET;
for x being Subset of ET
holds x in OP iff ex Y being Subset-Family of ET st Y c=OP & x = union Y
proof
let x being Subset of ET;
hereby
assume
A1: x in OP;
reconsider B={x} as Subset-Family of ET;
x=union B;
hence ex Y being Subset-Family of ET st Y c=OP & x = union Y
by A1,ZFMISC_1:31;
end;
given Y being Subset-Family of ET such that
A2: Y c=OP & x = union Y;
thus x in OP by A2,Th9;
end;
hence thesis;
end;
end;
definition
let ET being FMT_TopSpace;
let S being Subset-Family of ET;
attr S is open means S c= Family_open_set(ET);
end;
registration
let ET being FMT_TopSpace;
cluster open for Subset-Family of ET;
existence
proof
take Family_open_set(ET);
thus thesis;
end;
end;
registration
let ET being FMT_TopSpace;
cluster open quasi_basis for Subset-Family of ET;
existence
proof
take Family_open_set(ET);
thus thesis;
end;
end;
definition
let ET being FMT_TopSpace;
mode Basis of ET is open quasi_basis Subset-Family of ET;
end;
theorem
for ET being FMT_TopSpace, B being Basis of ET holds
Family_open_set(ET) = UniCl B
proof
let X be FMT_TopSpace, B be Basis of X;
thus Family_open_set(X) c= UniCl B by Def8;
hereby
let t be object;
assume t in UniCl B;
then consider Y be Subset-Family of X such that
A1: Y c= B & t=union Y by CANTOR_1:def 1;
B is open;
then B c= Family_open_set(X);
then Y c= Family_open_set(X) by A1;
hence t in Family_open_set(X) by A1,Th9;
end;
end;
theorem
for B being non empty Subset-Family of X st
(for B1,B2 being Element of B holds
ex BB being Subset of B st B1/\B2=union BB) & X = union B
holds
ex ET being FMT_TopSpace st the carrier of ET = X & B is Basis of ET
proof
let B be non empty Subset-Family of X such that
A1: (for B1,B2 be Element of B
ex BB being Subset of B st B1/\B2=union BB) and
A2: X = union B;
set O=UniCl B;
set T=TopStruct(#X,O#);
T is TopSpace by A1,A2,Th3;
then consider ET be FMT_TopSpace such that
A3: the carrier of T=the carrier of ET and
A4: Family_open_set(ET)=the topology of T by Th12;
reconsider B1=B as Subset-Family of ET by A3;
A5: B1 is open by A4,CANTOR_1:1;
B1 is quasi_basis by A3,A4;
hence thesis by A3,A5;
end;
theorem
for ET being FMT_TopSpace, B being Basis of ET holds
(for B1,B2 being Element of B holds
ex BB being Subset of B st B1 /\ B2 = union BB) &
(the carrier of ET = union B)
proof
let X be FMT_TopSpace, B be Basis of X;
A1: B is quasi_basis;
thus (for B1,B2 be Element of B holds
ex BB being Subset of B st B1/\B2=union BB)
proof
let B1,B2 be Element of B;
per cases;
suppose B is empty; then
A2: UniCl B ={{}} by YELLOW_9:16;
the carrier of X in Family_open_set(X) by Th9;
hence thesis by A1,A2,TARSKI:def 1;
end;
suppose
A3: not B is empty;
B is open;
then B c= Family_open_set(X);
then B1 in Family_open_set(X) & B2 in Family_open_set(X) by A3;
then B1/\B2 in Family_open_set(X) & B is quasi_basis by Th9;
then consider Y be Subset-Family of X such that
A4: Y c= B & B1/\B2 = union Y by CANTOR_1:def 1;
reconsider Y as Subset of B by A4;
thus ex BB being Subset of B st B1/\B2=union BB by A4;
end;
end;
the carrier of X in Family_open_set(X) by Th9;
then consider Y be Subset-Family of X such that
A5: Y c= B & the carrier of X=union Y by A1,CANTOR_1:def 1;
thus the carrier of X c= union B by A5,ZFMISC_1:77;
thus union B c= the carrier of X;
end;
begin :: Bijection between TopSpace and FMT_TopSpace
definition
let T being non empty TopSpace;
func TopSpace2FMT T -> FMT_TopSpace means
:Def9:
the carrier of it = the carrier of T &
Family_open_set(it) = the topology of T;
existence by Th12;
uniqueness
proof
let S1,S2 be FMT_TopSpace such that
A1: the carrier of S1 = the carrier of T &
Family_open_set(S1) = the topology of T and
A2: the carrier of S2 = the carrier of T &
Family_open_set(S2) = the topology of T;
set F1=the BNbd of S1;
set F2=the BNbd of S2;
F1=F2
proof
reconsider F2 as Function of the carrier of S1,
bool bool the carrier of S1 by A1,A2;
for x being object st x in the carrier of S1 holds F1.x=F2.x
proof
let x being object;
assume x in the carrier of S1;
then reconsider x as Element of S1;
F1.x=F2.x
proof
hereby
let t be object;
assume t in F1.x;
then t in U_FMT x;
then t in {V where V is Subset of S1:
ex O be Subset of T st O in the topology of T & x in O & O c= V}
by A1,Th13;
then consider V1 be Subset of S1 such that
A3: t=V1 and
A4: ex O be Subset of T st O in the topology of T & x in O & O c= V1;
consider O1 be Subset of T such that
A5: O1 in the topology of T & x in O1 & O1 c= V1 by A4;
reconsider V2=V1 as Subset of S2 by A1,A2;
reconsider x2=x as Element of S2 by A1,A2;
O1 in the topology of T & x2 in O1 & O1 c= V2 by A5;
then t in {V where V is Subset of S2:
ex O be Subset of T st O in the topology of T & x in O & O c= V}
by A3;
then t in U_FMT x2 by A2,Th13;
hence t in F2.x;
end;
let t be object;
assume
A6: t in F2.x;
consider x3 be Element of S2 such that
A7: x=x3 by A1,A2;
t in U_FMT x3 by A7,A6;
then t in {V where V is Subset of S2:
ex O be Subset of T st O in the topology of T & x3 in O & O c= V}
by A2,Th13;
then consider V2 be Subset of S2 such that
A8: t=V2 and
A9: ex O be Subset of T st O in the topology of T & x3 in O & O c= V2;
consider O2 be Subset of T such that
A10: O2 in the topology of T & x3 in O2 & O2 c= V2 by A9;
reconsider V1=V2 as Subset of S1 by A1,A2;
reconsider x1=x3 as Element of S1 by A1,A2;
O2 in the topology of T & x1 in O2 & O2 c= V1 by A10;
then t in {V where V is Subset of S1:
ex O be Subset of T st O in the topology of T & x in O & O c= V}
by A7,A8;
then t in U_FMT x1 by A7,A1,Th13;
hence t in F1.x by A7;
end;
hence thesis;
end;
hence thesis by FUNCT_2:12;
end;
hence S1=S2;
end;
end;
definition
let ET being FMT_TopSpace;
func FMT2TopSpace ET -> strict TopSpace means
:Def10:
the carrier of it = the carrier of ET &
Family_open_set(ET) = the topology of it;
existence
proof
set T=TopStruct(#the carrier of ET,Family_open_set(ET)#);
A1: ( for a being Subset-Family of T st a c= the topology of T holds
union a in the topology of T ) by Th9;
( for a, b being Subset of ET st
a in the topology of T & b in the topology of T holds
a /\ b in Family_open_set(ET) ) by Th9;
then T is TopSpace by A1,Th9,PRE_TOPC:def 1;
hence thesis;
end;
uniqueness;
end;
registration
let ET being FMT_TopSpace;
cluster FMT2TopSpace ET -> non empty;
coherence by Def10;
end;
theorem
for T being non empty strict TopSpace holds T = FMT2TopSpace TopSpace2FMT T
proof
let T be non empty strict TopSpace;
TopSpace2FMT T is FMT_TopSpace &
the carrier of TopSpace2FMT T=the carrier of T &
Family_open_set(TopSpace2FMT T)=the topology of T by Def9;
hence thesis by Def10;
end;
theorem
for ET being FMT_TopSpace holds ET = TopSpace2FMT FMT2TopSpace ET
proof
let ET be FMT_TopSpace;
FMT2TopSpace ET is strict TopSpace &
the carrier of FMT2TopSpace ET=the carrier of ET &
Family_open_set(ET)=the topology of FMT2TopSpace ET by Def10;
hence thesis by Def9;
end;