let X be non empty set ; :: thesis: for R being Equivalence_Relation of X holds TopSpace_induced_by (@ (uniformity_induced_by R)) = partition_topology (Class R)
let R be Equivalence_Relation of X; :: thesis: TopSpace_induced_by (@ (uniformity_induced_by R)) = partition_topology (Class R)
set T1 = TopSpace_induced_by (@ (uniformity_induced_by R));
set T2 = partition_topology (Class R);
now :: thesis: ( the carrier of (TopSpace_induced_by (@ (uniformity_induced_by R))) = the carrier of (partition_topology (Class R)) & the topology of (TopSpace_induced_by (@ (uniformity_induced_by R))) = the topology of (partition_topology (Class R)) )
thus the carrier of (TopSpace_induced_by (@ (uniformity_induced_by R))) = the carrier of (partition_topology (Class R)) by FINTOPO7:def 16; :: thesis: the topology of (TopSpace_induced_by (@ (uniformity_induced_by R))) = the topology of (partition_topology (Class R))
A1: the topology of (TopSpace_induced_by (@ (uniformity_induced_by R))) = Family_open_set (FMT_induced_by (@ (uniformity_induced_by R))) by FINTOPO7:def 16
.= { O where O is open Subset of (FMT_induced_by (@ (uniformity_induced_by R))) : verum } ;
A2: the topology of (partition_topology (Class R)) = { (union P) where P is Subset of (Class R) : verum } by Th14;
A3: the topology of (TopSpace_induced_by (@ (uniformity_induced_by R))) c= the topology of (partition_topology (Class R))
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in the topology of (TopSpace_induced_by (@ (uniformity_induced_by R))) or t in the topology of (partition_topology (Class R)) )
assume t in the topology of (TopSpace_induced_by (@ (uniformity_induced_by R))) ; :: thesis: t in the topology of (partition_topology (Class R))
then consider O being open Subset of (FMT_induced_by (@ (uniformity_induced_by R))) such that
A4: t = O by A1;
per cases ( O is empty or not O is empty ) ;
suppose A5: O is empty ; :: thesis: t in the topology of (partition_topology (Class R))
{} c= Class R ;
then reconsider P = {} as Subset of (Class R) ;
t = union P by A4, A5, ZFMISC_1:2;
hence t in the topology of (partition_topology (Class R)) by A2; :: thesis: verum
end;
suppose A6: not O is empty ; :: thesis: t in the topology of (partition_topology (Class R))
set P = { (Class (R,u)) where u is Element of O : verum } ;
{ (Class (R,u)) where u is Element of O : verum } c= Class R
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in { (Class (R,u)) where u is Element of O : verum } or u in Class R )
assume u in { (Class (R,u)) where u is Element of O : verum } ; :: thesis: u in Class R
then consider u0 being Element of O such that
A7: u = Class (R,u0) ;
A8: u0 in O by A6;
thus u in Class R by A7, A8, EQREL_1:def 3; :: thesis: verum
end;
then reconsider P = { (Class (R,u)) where u is Element of O : verum } as Subset of (Class R) ;
reconsider t1 = t as Subset of X by A4;
t1 = union P
proof
thus t1 c= union P :: according to XBOOLE_0:def 10 :: thesis: union P c= t1
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in t1 or a in union P )
assume A10: a in t1 ; :: thesis: a in union P
then reconsider b = a as Element of O by A4;
( b in Class (R,b) & Class (R,b) in P ) by A10, EQREL_1:20;
hence a in union P by TARSKI:def 4; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in union P or a in t1 )
assume a in union P ; :: thesis: a in t1
then consider Q being set such that
A11: a in Q and
A12: Q in P by TARSKI:def 4;
consider v being Element of O such that
A13: Q = Class (R,v) by A12;
v in O by A6;
then reconsider w = v as Element of (@ (uniformity_induced_by R)) ;
O in Neighborhood w by Th8, A6;
then consider V being Element of the entourages of (@ (uniformity_induced_by R)) such that
A14: O = Neighborhood (V,w) ;
V in rho R ;
then consider W being Relation of the carrier of (@ (uniformity_induced_by R)) such that
A15: V = W and
A16: R c= W ;
A17: ( Neighborhood (V,w) = V .: {w} & Neighborhood (V,w) = rng (V | {w}) & Neighborhood (V,w) = Im (V,w) & Neighborhood (V,w) = Class (V,w) & Neighborhood (V,w) = neighbourhood (,) ) by UNIFORM2:14;
Class (R,w) c= Class (W,w)
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Class (R,w) or z in Class (W,w) )
assume z in Class (R,w) ; :: thesis: z in Class (W,w)
then [w,z] in W by A16, EQREL_1:18;
hence z in Class (W,w) by EQREL_1:18; :: thesis: verum
end;
hence a in t1 by A11, A13, A4, A17, A15, A14; :: thesis: verum
end;
hence t in the topology of (partition_topology (Class R)) by A2; :: thesis: verum
end;
end;
end;
the topology of (partition_topology (Class R)) c= the topology of (TopSpace_induced_by (@ (uniformity_induced_by R)))
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in the topology of (partition_topology (Class R)) or t in the topology of (TopSpace_induced_by (@ (uniformity_induced_by R))) )
assume A18: t in the topology of (partition_topology (Class R)) ; :: thesis: t in the topology of (TopSpace_induced_by (@ (uniformity_induced_by R)))
then consider P being Subset of (Class R) such that
A19: t = union P by A2;
reconsider Q = union P as Subset of (FMT_induced_by (@ (uniformity_induced_by R))) by A18, A19;
for x being Element of (@ (uniformity_induced_by R)) st x in Q holds
Q in Neighborhood x
proof
let x be Element of (@ (uniformity_induced_by R)); :: thesis: ( x in Q implies Q in Neighborhood x )
assume A20: x in Q ; :: thesis: Q in Neighborhood x
then consider T being set such that
A21: x in T and
A22: T in P by TARSKI:def 4;
T in Class R by A22;
then consider b being object such that
A23: b in X and
A24: T = Class (R,b) by EQREL_1:def 3;
set S1 = { [x,y] where y is Element of Q : verum } ;
set S = R \/ { [x,y] where y is Element of Q : verum } ;
{ [x,y] where y is Element of Q : verum } c= [:X,X:]
proof
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in { [x,y] where y is Element of Q : verum } or s in [:X,X:] )
assume s in { [x,y] where y is Element of Q : verum } ; :: thesis: s in [:X,X:]
then consider y being Element of Q such that
A25: s = [x,y] ;
Q c= X ;
then y in X by A20;
hence s in [:X,X:] by A25, ZFMISC_1:def 2; :: thesis: verum
end;
then reconsider S = R \/ { [x,y] where y is Element of Q : verum } as Subset of [:X,X:] by XBOOLE_1:8;
R c= S by XBOOLE_1:7;
then S in rho R ;
then reconsider V = S as Element of the entourages of (@ (uniformity_induced_by R)) ;
Q = Neighborhood (V,x)
proof
thus Q c= Neighborhood (V,x) :: according to XBOOLE_0:def 10 :: thesis: Neighborhood (V,x) c= Q
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Q or a in Neighborhood (V,x) )
assume a in Q ; :: thesis: a in Neighborhood (V,x)
then reconsider b = a as Element of Q ;
A27: [x,b] in { [x,y] where y is Element of Q : verum } ;
A28: { [x,y] where y is Element of Q : verum } c= R \/ { [x,y] where y is Element of Q : verum } by XBOOLE_1:7;
b in Q by A20;
then reconsider c = b as Element of (@ (uniformity_induced_by R)) ;
[x,c] in V by A28, A27;
hence a in Neighborhood (V,x) ; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Neighborhood (V,x) or a in Q )
assume a in Neighborhood (V,x) ; :: thesis: a in Q
then consider y being Element of (@ (uniformity_induced_by R)) such that
A29: a = y and
A30: [x,y] in V ;
per cases ( [x,a] in { [x,y] where y is Element of Q : verum } or [x,a] in R ) by A29, A30, XBOOLE_0:def 3;
suppose [x,a] in { [x,y] where y is Element of Q : verum } ; :: thesis: a in Q
then consider y being Element of Q such that
A31: [x,a] = [x,y] ;
a = y by A31, XTUPLE_0:1;
hence a in Q by A20; :: thesis: verum
end;
end;
end;
hence Q in Neighborhood x ; :: thesis: verum
end;
then reconsider O = union P as open Subset of (FMT_induced_by (@ (uniformity_induced_by R))) by Th8;
t = O by A19;
hence t in the topology of (TopSpace_induced_by (@ (uniformity_induced_by R))) by A1; :: thesis: verum
end;
hence the topology of (TopSpace_induced_by (@ (uniformity_induced_by R))) = the topology of (partition_topology (Class R)) by A3; :: thesis: verum
end;
hence TopSpace_induced_by (@ (uniformity_induced_by R)) = partition_topology (Class R) ; :: thesis: verum