let q1, q2 be Point of (TOP-REAL 2); LSeg (q1,q2) is boundary
per cases
( q1 = q2 or q1 <> q2 )
;
suppose A1:
q1 <> q2
;
LSeg (q1,q2) is boundary set P =
LSeg (
q1,
q2);
the
carrier of
(TOP-REAL 2) c= Cl ((LSeg (q1,q2)) `)
proof
let z be
object ;
TARSKI:def 3 ( not z in the carrier of (TOP-REAL 2) or z in Cl ((LSeg (q1,q2)) `) )
assume A2:
z in the
carrier of
(TOP-REAL 2)
;
z in Cl ((LSeg (q1,q2)) `)
per cases
( z in LSeg (q1,q2) or not z in LSeg (q1,q2) )
;
suppose A3:
z in LSeg (
q1,
q2)
;
z in Cl ((LSeg (q1,q2)) `)reconsider ez =
z as
Point of
(Euclid 2) by A2, TOPREAL3:8;
set p1 =
q1 - q2;
consider s being
Real such that A4:
z = ((1 - s) * q1) + (s * q2)
and
0 <= s
and
s <= 1
by A3;
set p =
((1 - s) * q1) + (s * q2);
for
G1 being
Subset of
(TOP-REAL 2) st
G1 is
open &
z in G1 holds
(LSeg (q1,q2)) ` meets G1
proof
let G1 be
Subset of
(TOP-REAL 2);
( G1 is open & z in G1 implies (LSeg (q1,q2)) ` meets G1 )
assume A6:
G1 is
open
;
( not z in G1 or (LSeg (q1,q2)) ` meets G1 )
thus
(
z in G1 implies
(LSeg (q1,q2)) ` meets G1 )
verumproof
A7:
TopStruct(# the
carrier of
(TOP-REAL 2), the
topology of
(TOP-REAL 2) #)
= TopSpaceMetr (Euclid 2)
by EUCLID:def 8;
then reconsider GG =
G1 as
Subset of
(TopSpaceMetr (Euclid 2)) ;
assume A8:
z in G1
;
(LSeg (q1,q2)) ` meets G1
GG is
open
by A6, A7, PRE_TOPC:30;
then consider r being
Real such that A9:
r > 0
and A10:
Ball (
ez,
r)
c= G1
by A8, TOPMETR:15;
reconsider r =
r as
Real ;
A11:
r / 2
< r
by A9, XREAL_1:216;
set p2 =
(((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]|) + (((1 - s) * q1) + (s * q2));
now not (((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]|) + (((1 - s) * q1) + (s * q2)) in LSeg (q1,q2)assume
(((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]|) + (((1 - s) * q1) + (s * q2)) in LSeg (
q1,
q2)
;
contradictionthen consider s2 being
Real such that A12:
(((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]|) + (((1 - s) * q1) + (s * q2)) = ((1 - s2) * q1) + (s2 * q2)
and
0 <= s2
and
s2 <= 1
;
A13:
now not s - s2 = 0 assume
s - s2 = 0
;
contradictionthen
((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]| = (((1 - s) * q1) + (s * q2)) - (((1 - s) * q1) + (s * q2))
by A12, RLVECT_4:1;
then A14:
((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]| = 0. (TOP-REAL 2)
by RLVECT_1:5;
A15:
(r / 2) / |.(q1 - q2).| =
(r * (2 ")) * (|.(q1 - q2).| ")
by XCMPLX_0:def 9
.=
r * ((2 ") * (|.(q1 - q2).| "))
;
(2 ") * (|.(q1 - q2).| ") <> 0
by A5;
then
|[(- ((q1 - q2) `2)),((q1 - q2) `1)]| = 0. (TOP-REAL 2)
by A9, A14, A15, RLVECT_1:11, XCMPLX_1:6;
then A16:
(
(0. (TOP-REAL 2)) `1 = - ((q1 - q2) `2) &
(0. (TOP-REAL 2)) `2 = (q1 - q2) `1 )
by EUCLID:52;
(
(0. (TOP-REAL 2)) `1 = 0 &
(0. (TOP-REAL 2)) `2 = 0 )
by EUCLID:52, EUCLID:54;
hence
contradiction
by A1, A16, EUCLID:53, EUCLID:54, RLVECT_1:21;
verum end; A17:
((((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]|) + (((1 - s) * q1) + (s * q2))) - (((1 - s) * q1) + (s * q2)) = ((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]|
by RLVECT_4:1;
((((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]|) + (((1 - s) * q1) + (s * q2))) - (((1 - s) * q1) + (s * q2)) =
((((1 - s2) * q1) + (s2 * q2)) - ((1 - s) * q1)) - (s * q2)
by A12, RLVECT_1:27
.=
((((1 - s2) * q1) - ((1 - s) * q1)) + (s2 * q2)) - (s * q2)
by RLVECT_1:def 3
.=
((((1 - s2) - (1 - s)) * q1) + (s2 * q2)) - (s * q2)
by RLVECT_1:35
.=
((s - s2) * q1) + ((s2 * q2) - (s * q2))
by RLVECT_1:def 3
.=
((s - s2) * q1) + ((s2 - s) * q2)
by RLVECT_1:35
.=
((s - s2) * q1) + ((- (s - s2)) * q2)
.=
((s - s2) * q1) - ((s - s2) * q2)
by RLVECT_1:79
.=
(s - s2) * (q1 - q2)
by RLVECT_1:34
;
then
((1 / (s - s2)) * (s - s2)) * (q1 - q2) = (1 / (s - s2)) * (((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]|)
by A17, RLVECT_1:def 7;
then
1
* (q1 - q2) = (1 / (s - s2)) * (((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]|)
by A13, XCMPLX_1:106;
then
q1 - q2 = (1 / (s - s2)) * (((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]|)
by RLVECT_1:def 8;
then A18:
q1 - q2 = ((1 / (s - s2)) * ((r / 2) / |.(q1 - q2).|)) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]|
by RLVECT_1:def 7;
(
(q1 - q2) `1 = |[(- ((q1 - q2) `2)),((q1 - q2) `1)]| `2 &
- ((q1 - q2) `2) = |[(- ((q1 - q2) `2)),((q1 - q2) `1)]| `1 )
by EUCLID:52;
then
q1 - q2 = 0. (TOP-REAL 2)
by A18, Th84;
hence
contradiction
by A1, RLVECT_1:21;
verum end;
then A19:
(((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]|) + (((1 - s) * q1) + (s * q2)) in the
carrier of
(TOP-REAL 2) \ (LSeg (q1,q2))
by XBOOLE_0:def 5;
reconsider ep2 =
(((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]|) + (((1 - s) * q1) + (s * q2)) as
Point of
(Euclid 2) by TOPREAL3:8;
A20:
((((1 - s) * q1) + (s * q2)) + (- (((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]|))) - (((1 - s) * q1) + (s * q2)) = - (((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]|)
by RLVECT_4:1;
A21:
(
|[(- ((q1 - q2) `2)),((q1 - q2) `1)]| `1 = - ((q1 - q2) `2) &
|[(- ((q1 - q2) `2)),((q1 - q2) `1)]| `2 = (q1 - q2) `1 )
by EUCLID:52;
|.((((1 - s) * q1) + (s * q2)) - ((((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]|) + (((1 - s) * q1) + (s * q2)))).| =
|.(((((1 - s) * q1) + (s * q2)) - (((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]|)) - (((1 - s) * q1) + (s * q2))).|
by RLVECT_1:27
.=
|.(- (((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]|)).|
by A20
.=
|.(((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]|).|
by TOPRNS_1:26
.=
|.((r / 2) / |.(q1 - q2).|).| * |.|[(- ((q1 - q2) `2)),((q1 - q2) `1)]|.|
by TOPRNS_1:7
.=
|.((r / 2) / |.(q1 - q2).|).| * (sqrt (((- ((q1 - q2) `2)) ^2) + (((q1 - q2) `1) ^2)))
by A21, JGRAPH_1:30
.=
|.((r / 2) / |.(q1 - q2).|).| * (sqrt ((((q1 - q2) `1) ^2) + (((q1 - q2) `2) ^2)))
.=
|.((r / 2) / |.(q1 - q2).|).| * |.(q1 - q2).|
by JGRAPH_1:30
.=
(|.(r / 2).| / |.|.(q1 - q2).|.|) * |.(q1 - q2).|
by COMPLEX1:67
.=
(|.(r / 2).| / |.(q1 - q2).|) * |.(q1 - q2).|
by ABSVALUE:def 1
.=
|.(r / 2).|
by A5, XCMPLX_1:87
.=
r / 2
by A9, ABSVALUE:def 1
;
then
dist (
ez,
ep2)
< r
by A4, A11, JGRAPH_1:28;
then
(((r / 2) / |.(q1 - q2).|) * |[(- ((q1 - q2) `2)),((q1 - q2) `1)]|) + (((1 - s) * q1) + (s * q2)) in Ball (
ez,
r)
by METRIC_1:11;
hence
(LSeg (q1,q2)) ` meets G1
by A10, A19, XBOOLE_0:3;
verum
end;
end; hence
z in Cl ((LSeg (q1,q2)) `)
by A2, PRE_TOPC:def 7;
verum end; end;
end; then
Cl ((LSeg (q1,q2)) `) = [#] (TOP-REAL 2)
;
then
(LSeg (q1,q2)) ` is
dense
by TOPS_1:def 3;
hence
LSeg (
q1,
q2) is
boundary
by TOPS_1:def 4;
verum end; end;