:: On the Characterization of {H}ausdorff Spaces
:: by Artur Korni{\l}owicz
::
:: Received April 18, 1998
:: Copyright (c) 1998 Association of Mizar Users
Lm1:
now
let S,
T,
x1,
x2 be
set ;
:: thesis: ( x1 in S & x2 in T implies <:(pr2 S,T),(pr1 S,T):> . x1,x2 = [x2,x1] )assume A1:
(
x1 in S &
x2 in T )
;
:: thesis: <:(pr2 S,T),(pr1 S,T):> . x1,x2 = [x2,x1]A2:
dom <:(pr2 S,T),(pr1 S,T):> =
(dom (pr2 S,T)) /\ (dom (pr1 S,T))
by FUNCT_3:def 8
.=
(dom (pr2 S,T)) /\ [:S,T:]
by FUNCT_3:def 5
.=
[:S,T:] /\ [:S,T:]
by FUNCT_3:def 6
.=
[:S,T:]
;
[x1,x2] in [:S,T:]
by A1, ZFMISC_1:106;
hence <:(pr2 S,T),(pr1 S,T):> . x1,
x2 =
[((pr2 S,T) . x1,x2),((pr1 S,T) . x1,x2)]
by A2, FUNCT_3:def 8
.=
[x2,((pr1 S,T) . x1,x2)]
by A1, FUNCT_3:def 6
.=
[x2,x1]
by A1, FUNCT_3:def 5
;
:: thesis: verum
end;
theorem :: YELLOW12:1
theorem Th2: :: YELLOW12:2
theorem :: YELLOW12:3
theorem Th4: :: YELLOW12:4
theorem Th5: :: YELLOW12:5
theorem :: YELLOW12:6
theorem Th7: :: YELLOW12:7
theorem Th8: :: YELLOW12:8
theorem Th9: :: YELLOW12:9
theorem Th10: :: YELLOW12:10
theorem Th11: :: YELLOW12:11
theorem :: YELLOW12:12
theorem Th13: :: YELLOW12:13
theorem :: YELLOW12:14
theorem :: YELLOW12:15
theorem :: YELLOW12:16
theorem :: YELLOW12:17
theorem :: YELLOW12:18
theorem :: YELLOW12:19
theorem :: YELLOW12:20
theorem :: YELLOW12:21
theorem :: YELLOW12:22
theorem :: YELLOW12:23
theorem Th24: :: YELLOW12:24
theorem Th25: :: YELLOW12:25
theorem :: YELLOW12:26
theorem :: YELLOW12:27
theorem :: YELLOW12:28
theorem :: YELLOW12:29
theorem :: YELLOW12:30
theorem :: YELLOW12:31
theorem Th32: :: YELLOW12:32
theorem Th33: :: YELLOW12:33
theorem Th34: :: YELLOW12:34
theorem Th35: :: YELLOW12:35
theorem :: YELLOW12:36
theorem Th37: :: YELLOW12:37
theorem Th38: :: YELLOW12:38
theorem Th39: :: YELLOW12:39
theorem Th40: :: YELLOW12:40
theorem Th41: :: YELLOW12:41
theorem Th42: :: YELLOW12:42
theorem Th43: :: YELLOW12:43
theorem :: YELLOW12:44
theorem Th45: :: YELLOW12:45
theorem :: YELLOW12:46
theorem :: YELLOW12:47
theorem Th48: :: YELLOW12:48
for
S1,
S2,
T1,
T2 being non
empty TopSpace for
R being
Refinement of
[:S1,T1:],
[:S2,T2:] st the
carrier of
S1 = the
carrier of
S2 & the
carrier of
T1 = the
carrier of
T2 holds
{ ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } is
Basis of
R
theorem Th49: :: YELLOW12:49
for
S1,
S2,
T1,
T2 being non
empty TopSpace for
R being
Refinement of
[:S1,T1:],
[:S2,T2:] for
R1 being
Refinement of
S1,
S2 for
R2 being
Refinement of
T1,
T2 st the
carrier of
S1 = the
carrier of
S2 & the
carrier of
T1 = the
carrier of
T2 holds
( the
carrier of
[:R1,R2:] = the
carrier of
R & the
topology of
[:R1,R2:] = the
topology of
R )
theorem :: YELLOW12:50