let T be non empty TopSpace; ( T is Hausdorff iff for N being net of T
for p, q being Point of T st p in Lim N & q in Lim N holds
p = q )
thus
( T is Hausdorff implies for N being net of T
for p, q being Point of T st p in Lim N & q in Lim N holds
p = q )
( ( for N being net of T
for p, q being Point of T st p in Lim N & q in Lim N holds
p = q ) implies T is Hausdorff )proof
assume A1:
T is
Hausdorff
;
for N being net of T
for p, q being Point of T st p in Lim N & q in Lim N holds
p = q
let N be
net of
T;
for p, q being Point of T st p in Lim N & q in Lim N holds
p = q
given p1,
p2 being
Point of
T such that A2:
p1 in Lim N
and A3:
p2 in Lim N
and A4:
p1 <> p2
;
contradiction
consider W,
V being
Subset of
T such that A5:
W is
open
and A6:
V is
open
and A7:
p1 in W
and A8:
p2 in V
and A9:
W misses V
by A1, A4;
V is
a_neighborhood of
p2
by A6, A8, CONNSP_2:3;
then A10:
N is_eventually_in V
by A3, Def15;
W is
a_neighborhood of
p1
by A5, A7, CONNSP_2:3;
then
N is_eventually_in W
by A2, Def15;
hence
contradiction
by A9, A10, Th17;
verum
end;
assume A11:
for N being net of T
for p, q being Point of T st p in Lim N & q in Lim N holds
p = q
; T is Hausdorff
given p, q being Point of T such that A12:
p <> q
and
A13:
for W, V being Subset of T st W is open & V is open & p in W & q in V holds
W meets V
; PRE_TOPC:def 10 contradiction
set pN = [:(OpenNeighborhoods p),(OpenNeighborhoods q):];
set cT = the carrier of T;
set cpN = the carrier of [:(OpenNeighborhoods p),(OpenNeighborhoods q):];
deffunc H1( Element of the carrier of [:(OpenNeighborhoods p),(OpenNeighborhoods q):]) -> set = ($1 `1) /\ ($1 `2);
A14:
for i being Element of the carrier of [:(OpenNeighborhoods p),(OpenNeighborhoods q):] holds the carrier of T meets H1(i)
consider f being Function of the carrier of [:(OpenNeighborhoods p),(OpenNeighborhoods q):], the carrier of T such that
A19:
for i being Element of the carrier of [:(OpenNeighborhoods p),(OpenNeighborhoods q):] holds f . i in H1(i)
from FUNCT_2:sch 10(A14);
reconsider N = NetStr(# the carrier of [:(OpenNeighborhoods p),(OpenNeighborhoods q):], the InternalRel of [:(OpenNeighborhoods p),(OpenNeighborhoods q):],f #) as net of T by Lm1, Lm2;
A20:
the carrier of [:(OpenNeighborhoods p),(OpenNeighborhoods q):] = [: the carrier of (OpenNeighborhoods p), the carrier of (OpenNeighborhoods q):]
by YELLOW_3:def 2;
now for V being a_neighborhood of q holds N is_eventually_in Vlet V be
a_neighborhood of
q;
N is_eventually_in VA21:
N is_eventually_in Int V
proof
A22:
[#] T in the
carrier of
(OpenNeighborhoods p)
by Th30;
(
q in Int V &
Int V is
open )
by CONNSP_2:def 1;
then
Int V in the
carrier of
(OpenNeighborhoods q)
by Th30;
then reconsider i =
[([#] T),(Int V)] as
Element of
N by A20, A22, ZFMISC_1:87;
take
i
;
WAYBEL_0:def 11 for b1 being Element of the carrier of N holds
( not i <= b1 or N . b1 in Int V )
let j be
Element of
N;
( not i <= j or N . j in Int V )
reconsider j9 =
j,
i9 =
i as
Element of
[:(OpenNeighborhoods p),(OpenNeighborhoods q):] ;
consider j1 being
Element of
(OpenNeighborhoods p),
j2 being
Element of
(OpenNeighborhoods q) such that A23:
j = [j1,j2]
by A20, DOMAIN_1:1;
A24:
j `2 = j2
by A23;
consider W1 being
Subset of
T such that A25:
j1 = W1
and
p in W1
and
W1 is
open
by Th29;
consider W2 being
Subset of
T such that A26:
j2 = W2
and
q in W2
and
W2 is
open
by Th29;
assume
i <= j
;
N . j in Int V
then
[i,j] in the
InternalRel of
[:(OpenNeighborhoods p),(OpenNeighborhoods q):]
by ORDERS_2:def 5;
then
i9 <= j9
by ORDERS_2:def 5;
then
(
i9 `2 = Int V &
i9 `2 <= j9 `2 )
by YELLOW_3:12;
then
W2 c= Int V
by A24, A26, Th31;
then A27:
W1 /\ W2 c= (Int V) /\ ([#] T)
by XBOOLE_1:27;
j `1 = j1
by A23;
then
f . j in W1 /\ W2
by A19, A24, A25, A26;
then
f . j in (Int V) /\ ([#] T)
by A27;
hence
N . j in Int V
by XBOOLE_1:28;
verum
end;
Int V c= V
by TOPS_1:16;
hence
N is_eventually_in V
by A21, WAYBEL_0:8;
verum end;
then A28:
q in Lim N
by Def15;
now for V being a_neighborhood of p holds N is_eventually_in Vlet V be
a_neighborhood of
p;
N is_eventually_in VA29:
N is_eventually_in Int V
proof
A30:
[#] T in the
carrier of
(OpenNeighborhoods q)
by Th30;
(
p in Int V &
Int V is
open )
by CONNSP_2:def 1;
then
Int V in the
carrier of
(OpenNeighborhoods p)
by Th30;
then reconsider i =
[(Int V),([#] T)] as
Element of
N by A20, A30, ZFMISC_1:87;
take
i
;
WAYBEL_0:def 11 for b1 being Element of the carrier of N holds
( not i <= b1 or N . b1 in Int V )
let j be
Element of
N;
( not i <= j or N . j in Int V )
reconsider j9 =
j,
i9 =
i as
Element of
[:(OpenNeighborhoods p),(OpenNeighborhoods q):] ;
consider j1 being
Element of
(OpenNeighborhoods p),
j2 being
Element of
(OpenNeighborhoods q) such that A31:
j = [j1,j2]
by A20, DOMAIN_1:1;
A32:
j `1 = j1
by A31;
consider W2 being
Subset of
T such that A33:
j2 = W2
and
q in W2
and
W2 is
open
by Th29;
consider W1 being
Subset of
T such that A34:
j1 = W1
and
p in W1
and
W1 is
open
by Th29;
assume
i <= j
;
N . j in Int V
then
[i,j] in the
InternalRel of
[:(OpenNeighborhoods p),(OpenNeighborhoods q):]
by ORDERS_2:def 5;
then
i9 <= j9
by ORDERS_2:def 5;
then
(
i9 `1 = Int V &
i9 `1 <= j9 `1 )
by YELLOW_3:12;
then
W1 c= Int V
by A32, A34, Th31;
then A35:
W1 /\ W2 c= (Int V) /\ ([#] T)
by XBOOLE_1:27;
j `2 = j2
by A31;
then
f . j in W1 /\ W2
by A19, A32, A34, A33;
then
f . j in (Int V) /\ ([#] T)
by A35;
hence
N . j in Int V
by XBOOLE_1:28;
verum
end;
Int V c= V
by TOPS_1:16;
hence
N is_eventually_in V
by A29, WAYBEL_0:8;
verum end;
then
p in Lim N
by Def15;
hence
contradiction
by A11, A12, A28; verum