let T be non empty TopSpace; :: thesis: ( 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 )
:: thesis: ( ( 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
;
:: thesis: 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;
:: thesis: 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
;
:: thesis: 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, PRE_TOPC:def 16;
W is
a_neighborhood of
p1
by A5, A7, CONNSP_2:5;
then A10:
N is_eventually_in W
by A2, Def18;
V is
a_neighborhood of
p2
by A6, A8, CONNSP_2:5;
then
N is_eventually_in V
by A3, Def18;
hence
contradiction
by A9, A10, Th26;
:: thesis: 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
; :: thesis: 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
; :: according to PRE_TOPC:def 16 :: thesis: contradiction
set pN = [:(OpenNeighborhoods p),(OpenNeighborhoods q):];
set cT = the carrier of T;
set cpN = the carrier of [:(OpenNeighborhoods p),(OpenNeighborhoods q):];
A14:
the carrier of [:(OpenNeighborhoods p),(OpenNeighborhoods q):] = [:the carrier of (OpenNeighborhoods p),the carrier of (OpenNeighborhoods q):]
by YELLOW_3:def 2;
deffunc H1( Element of the carrier of [:(OpenNeighborhoods p),(OpenNeighborhoods q):]) -> set = ($1 `1 ) /\ ($1 `2 );
A15:
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 11(A15);
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;
now let V be
a_neighborhood of
p;
:: thesis: N is_eventually_in VA20:
Int V c= V
by TOPS_1:44;
N is_eventually_in Int V
proof
(
p in Int V &
Int V is
open )
by CONNSP_2:def 1, TOPS_1:51;
then A21:
Int V in the
carrier of
(OpenNeighborhoods p)
by Th39;
(
q in [#] T &
[#] T is
open )
by TOPS_1:53;
then
[#] T in the
carrier of
(OpenNeighborhoods q)
by Th39;
then reconsider i =
[(Int V),([#] T)] as
Element of
N by A14, A21, ZFMISC_1:106;
take
i
;
:: according to WAYBEL_0:def 11 :: thesis: 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;
:: thesis: ( not i <= j or N . j in Int V )
consider j1 being
Element of
(OpenNeighborhoods p),
j2 being
Element of
(OpenNeighborhoods q) such that A22:
j = [j1,j2]
by A14, DOMAIN_1:9;
A23:
(
j `1 = j1 &
j `2 = j2 )
by A22, MCART_1:7;
consider W1 being
Subset of
T such that A24:
(
j1 = W1 &
p in W1 &
W1 is
open )
by Th38;
consider W2 being
Subset of
T such that A25:
(
j2 = W2 &
q in W2 &
W2 is
open )
by Th38;
reconsider j' =
j,
i' =
i as
Element of
[:(OpenNeighborhoods p),(OpenNeighborhoods q):] ;
A26:
(
i' `1 = Int V &
i' `2 = [#] T )
by MCART_1:7;
assume
i <= j
;
:: thesis: N . j in Int V
then
[i,j] in the
InternalRel of
[:(OpenNeighborhoods p),(OpenNeighborhoods q):]
by ORDERS_2:def 9;
then
i' <= j'
by ORDERS_2:def 9;
then
(
i' `1 <= j' `1 &
i' `2 <= j' `2 )
by YELLOW_3:12;
then A27:
(
W1 c= Int V &
W2 c= [#] T )
by A23, A24, A26, Th40;
A28:
f . j in W1 /\ W2
by A19, A23, A24, A25;
W1 /\ W2 c= (Int V) /\ ([#] T)
by A27, XBOOLE_1:27;
then
f . j in (Int V) /\ ([#] T)
by A28;
hence
N . j in Int V
by XBOOLE_1:28;
:: thesis: verum
end; hence
N is_eventually_in V
by A20, WAYBEL_0:8;
:: thesis: verum end;
then A29:
p in Lim N
by Def18;
now let V be
a_neighborhood of
q;
:: thesis: N is_eventually_in VA30:
Int V c= V
by TOPS_1:44;
N is_eventually_in Int V
proof
(
q in Int V &
Int V is
open )
by CONNSP_2:def 1, TOPS_1:51;
then A31:
Int V in the
carrier of
(OpenNeighborhoods q)
by Th39;
(
p in [#] T &
[#] T is
open )
by TOPS_1:53;
then
[#] T in the
carrier of
(OpenNeighborhoods p)
by Th39;
then reconsider i =
[([#] T),(Int V)] as
Element of
N by A14, A31, ZFMISC_1:106;
take
i
;
:: according to WAYBEL_0:def 11 :: thesis: 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;
:: thesis: ( not i <= j or N . j in Int V )
consider j1 being
Element of
(OpenNeighborhoods p),
j2 being
Element of
(OpenNeighborhoods q) such that A32:
j = [j1,j2]
by A14, DOMAIN_1:9;
A33:
(
j `1 = j1 &
j `2 = j2 )
by A32, MCART_1:7;
consider W1 being
Subset of
T such that A34:
(
j1 = W1 &
p in W1 &
W1 is
open )
by Th38;
consider W2 being
Subset of
T such that A35:
(
j2 = W2 &
q in W2 &
W2 is
open )
by Th38;
reconsider j' =
j,
i' =
i as
Element of
[:(OpenNeighborhoods p),(OpenNeighborhoods q):] ;
A36:
(
i' `1 = [#] T &
i' `2 = Int V )
by MCART_1:7;
assume
i <= j
;
:: thesis: N . j in Int V
then
[i,j] in the
InternalRel of
[:(OpenNeighborhoods p),(OpenNeighborhoods q):]
by ORDERS_2:def 9;
then
i' <= j'
by ORDERS_2:def 9;
then
(
i' `1 <= j' `1 &
i' `2 <= j' `2 )
by YELLOW_3:12;
then A37:
(
W1 c= [#] T &
W2 c= Int V )
by A33, A35, A36, Th40;
A38:
f . j in W1 /\ W2
by A19, A33, A34, A35;
W1 /\ W2 c= (Int V) /\ ([#] T)
by A37, XBOOLE_1:27;
then
f . j in (Int V) /\ ([#] T)
by A38;
hence
N . j in Int V
by XBOOLE_1:28;
:: thesis: verum
end; hence
N is_eventually_in V
by A30, WAYBEL_0:8;
:: thesis: verum end;
then
q in Lim N
by Def18;
hence
contradiction
by A11, A12, A29; :: thesis: verum