let n be Nat; RAT n is dense Subset of (TOP-REAL n)
RAT n is Subset of (REAL n)
by NUMBERS:12, Th5;
then reconsider RATN = RAT n as Subset of (TOP-REAL n) by EUCLID:22;
for Q being Subset of (TOP-REAL n) st Q <> {} & Q is open holds
RATN meets Q
proof
let Q be
Subset of
(TOP-REAL n);
( Q <> {} & Q is open implies RATN meets Q )
assume that A1:
Q <> {}
and A2:
Q is
open
;
RATN meets Q
consider q being
object such that A3:
q in Q
by A1, XBOOLE_0:def 1;
TopStruct(# the
carrier of
(TOP-REAL n), the
topology of
(TOP-REAL n) #)
= TopSpaceMetr (Euclid n)
by EUCLID:def 8;
then reconsider Q0 =
Q as
Subset of
(TopSpaceMetr (Euclid n)) ;
reconsider q0 =
q as
Point of
(Euclid n) by A3, EUCLID:67;
Q0 is
open
by A2, Th10;
then consider m being non
zero Element of
NAT such that A6:
OpenHypercube (
q0,
(1 / m))
c= Q0
by A3, EUCLID_9:23;
set OH =
OpenHypercube (
q0,
(1 / m));
set f =
Intervals (
q0,
(1 / m));
A7:
dom (Intervals (q0,(1 / m))) = dom q0
by EUCLID_9:def 3;
A8:
for
x being
object st
x in dom (Intervals (q0,(1 / m))) holds
ex
k being
Element of
RAT st
k in (Intervals (q0,(1 / m))) . x
proof
let x be
object ;
( x in dom (Intervals (q0,(1 / m))) implies ex k being Element of RAT st k in (Intervals (q0,(1 / m))) . x )
assume A9:
x in dom (Intervals (q0,(1 / m)))
;
ex k being Element of RAT st k in (Intervals (q0,(1 / m))) . x
reconsider FF =
].((q0 . x) - (1 / m)),((q0 . x) + (1 / m)).[ as
open Subset of
R^1 by BORSUK_5:39;
A10:
(q0 . x) - (1 / m) < q0 . x
by XREAL_1:44;
q0 . x < (q0 . x) + (1 / m)
by XREAL_1:29;
then
(q0 . x) - (1 / m) < (q0 . x) + (1 / m)
by A10, XXREAL_0:2;
then
(
FF <> {} &
FF is
open )
by XXREAL_1:33;
then
FF meets RAT
by TOPGEN_1:51, TOPS_1:45;
then consider k being
object such that A11:
(
k in FF &
k in RAT )
by XBOOLE_0:3;
take
k
;
( k is set & k is Element of RAT & k in (Intervals (q0,(1 / m))) . x )
thus
(
k is
set &
k is
Element of
RAT &
k in (Intervals (q0,(1 / m))) . x )
by A11, A9, A7, EUCLID_9:def 3;
verum
end;
q in TOP-REAL n
by A3;
then
q in REAL n
by EUCLID:22;
then reconsider q1 =
q as
FinSequence of
REAL by FINSEQ_2:131;
A12:
dom q1 = Seg n
by A3, FINSEQ_1:89;
defpred S1[
object ,
object ]
means ( $2
in (Intervals (q0,(1 / m))) . $1 & $2 is
Element of
RAT );
A13:
for
x being
Nat st
x in Seg n holds
ex
y being
object st
S1[
x,
y]
consider p being
FinSequence such that A15:
dom p = Seg n
and A16:
for
k being
Nat st
k in Seg n holds
S1[
k,
p . k]
from FINSEQ_1:sch 1(A13);
A17:
p is
n -element
p is
Tuple of
n,
RAT
then A20:
p in RAT n
by FINSEQ_2:131;
p in OpenHypercube (
q0,
(1 / m))
hence
RATN meets Q
by A6, A20, XBOOLE_0:3;
verum
end;
hence
RAT n is dense Subset of (TOP-REAL n)
by TOPS_1:45; verum