:: Projections in n-Dimensional Euclidean Space to Each Coordinates
:: by Roman Matuszewski and Yatsuka Nakamura
::
:: Received November 3, 1997
:: Copyright (c) 1997-2016 Association of Mizar Users

environ

vocabularies HIDDEN, NUMBERS, REAL_1, SUBSET_1, XBOOLE_0, PRE_TOPC, EUCLID, NAT_1, FINSEQ_1, PARTFUN1, RELAT_1, FUNCT_1, TOPMETR, STRUCT_0, SUPINF_2, CARD_1, FINSEQ_2, ARYTM_1, ARYTM_3, XXREAL_0, RFINSEQ, CARD_3, FUNCT_4, ORDINAL4, COMPLEX1, SQUARE_1, RVSUM_1, RCOMP_1, PCOMPS_1, METRIC_1, TARSKI, ORDINAL2, TOPS_2, VALUED_1, MCART_1, FUNCT_2;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, RVSUM_1, FUNCT_1, PARTFUN1, RELSET_1, FINSEQ_1, FUNCT_2, BINOP_1, RFINSEQ, FINSEQ_2, NAT_D, VALUED_0, STRUCT_0, TOPS_2, SQUARE_1, FUNCT_7, TOPMETR, PRE_TOPC, METRIC_1, RLVECT_1, EUCLID, PSCOMP_1, PCOMPS_1, FINSEQOP, XXREAL_0;
definitions TARSKI, RELAT_1;
theorems TARSKI, EUCLID, TOPMETR, TOPS_1, METRIC_1, FUNCT_1, RFINSEQ, FUNCT_2, RELAT_1, TBSP_1, NAT_1, FINSEQ_3, FINSEQ_1, ABSVALUE, SQUARE_1, FINSEQ_2, TOPS_2, RVSUM_1, TOPREAL3, FUNCOP_1, FINSEQ_4, FUNCT_7, SEQ_2, PSCOMP_1, XREAL_0, XBOOLE_0, COMPLEX1, XREAL_1, XXREAL_0, FINSOP_1, PARTFUN1, NAT_D, VALUED_1, PRE_TOPC, CARD_1;
schemes FUNCT_2;
registrations XBOOLE_0, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, STRUCT_0, METRIC_1, PCOMPS_1, EUCLID, TOPMETR, VALUED_0, FINSEQ_1, MONOID_0, RELSET_1, FUNCT_2, SQUARE_1, RVSUM_1, PRE_POLY, FUNCT_7, ORDINAL1;
constructors HIDDEN, REAL_1, SQUARE_1, FINSEQOP, FINSEQ_4, FINSOP_1, RFINSEQ, NAT_D, FUNCT_7, TOPS_2, TOPMETR, PSCOMP_1, BINOP_2, FUNCSDOM, MONOID_0, PCOMPS_1, PRE_POLY;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities EUCLID, FINSEQ_2, RVSUM_1, SQUARE_1, STRUCT_0, VALUED_1;
expansions TARSKI;


Lm1: for n, i being Nat
for p being Element of (TOP-REAL n) ex q being Real ex g being FinSequence of REAL st
( g = p & q = g /. i )
proof end;

registration
let n be Nat;
cluster -> REAL -valued for Element of the carrier of (TOP-REAL n);
coherence
for b1 being Element of (TOP-REAL n) holds b1 is REAL -valued
proof end;
end;

theorem :: JORDAN2B:1
for i being Element of NAT
for n being Nat ex f being Function of (TOP-REAL n),R^1 st
for p being Element of (TOP-REAL n) holds f . p = p /. i
proof end;

theorem :: JORDAN2B:2
for n, i being Element of NAT st i in Seg n holds
(0. (TOP-REAL n)) /. i = 0
proof end;

theorem :: JORDAN2B:3
for n being Element of NAT
for r being Real
for p being Point of (TOP-REAL n)
for i being Element of NAT st i in Seg n holds
(r * p) /. i = r * (p /. i)
proof end;

theorem :: JORDAN2B:4
for n being Element of NAT
for p being Point of (TOP-REAL n)
for i being Element of NAT st i in Seg n holds
(- p) /. i = - (p /. i)
proof end;

theorem :: JORDAN2B:5
for n being Element of NAT
for p1, p2 being Point of (TOP-REAL n)
for i being Element of NAT st i in Seg n holds
(p1 + p2) /. i = (p1 /. i) + (p2 /. i)
proof end;

theorem Th6: :: JORDAN2B:6
for n being Element of NAT
for p1, p2 being Point of (TOP-REAL n)
for i being Element of NAT st i in Seg n holds
(p1 - p2) /. i = (p1 /. i) - (p2 /. i)
proof end;

theorem Th7: :: JORDAN2B:7
for n, i being Element of NAT st i <= n holds
(0* n) | i = 0* i
proof end;

theorem Th8: :: JORDAN2B:8
for n, i being Element of NAT holds (0* n) /^ i = 0* (n -' i)
proof end;

theorem Th9: :: JORDAN2B:9
for i being Element of NAT holds Sum (0* i) = 0
proof end;

theorem Th10: :: JORDAN2B:10
for n, i being Element of NAT
for r being Real st i in Seg n holds
Sum ((0* n) +* (i,r)) = r
proof end;

theorem Th11: :: JORDAN2B:11
for n being Element of NAT
for q being Element of REAL n
for p being Point of (TOP-REAL n)
for i being Element of NAT st i in Seg n & q = p holds
( p /. i <= |.q.| & (p /. i) ^2 <= |.q.| ^2 )
proof end;

theorem Th12: :: JORDAN2B:12
for n being Element of NAT
for s1 being Real
for P being Subset of (TOP-REAL n)
for i being Element of NAT st P = { p where p is Point of (TOP-REAL n) : s1 > p /. i } & i in Seg n holds
P is open
proof end;

theorem Th13: :: JORDAN2B:13
for n being Element of NAT
for s1 being Real
for P being Subset of (TOP-REAL n)
for i being Element of NAT st P = { p where p is Point of (TOP-REAL n) : s1 < p /. i } & i in Seg n holds
P is open
proof end;

theorem Th14: :: JORDAN2B:14
for n being Element of NAT
for P being Subset of (TOP-REAL n)
for a, b being Real
for i being Element of NAT st P = { p where p is Element of (TOP-REAL n) : ( a < p /. i & p /. i < b ) } & i in Seg n holds
P is open
proof end;

theorem Th15: :: JORDAN2B:15
for n being Element of NAT
for a, b being Real
for f being Function of (TOP-REAL n),R^1
for i being Element of NAT st ( for p being Element of (TOP-REAL n) holds f . p = p /. i ) holds
f " { s where s is Real : ( a < s & s < b ) } = { p where p is Element of (TOP-REAL n) : ( a < p /. i & p /. i < b ) }
proof end;

theorem Th16: :: JORDAN2B:16
for X being non empty TopSpace
for M being non empty MetrSpace
for f being Function of X,(TopSpaceMetr M) st ( for r being Real
for u being Element of M
for P being Subset of (TopSpaceMetr M) st r > 0 & P = Ball (u,r) holds
f " P is open ) holds
f is continuous
proof end;

theorem Th17: :: JORDAN2B:17
for u being Point of RealSpace
for r, u1 being Real st u1 = u holds
Ball (u,r) = { s where s is Real : ( u1 - r < s & s < u1 + r ) }
proof end;

theorem Th18: :: JORDAN2B:18
for n being Element of NAT
for f being Function of (TOP-REAL n),R^1
for i being Element of NAT st i in Seg n & ( for p being Element of (TOP-REAL n) holds f . p = p /. i ) holds
f is continuous
proof end;

theorem :: JORDAN2B:19
for s being Real holds abs <*s*> = <*|.s.|*>
proof end;

theorem Th20: :: JORDAN2B:20
for p being Element of (TOP-REAL 1) ex r being Real st p = <*r*>
proof end;

notation
let r be Real;
synonym |[r]| for <*r*>;
end;

definition
let r be Real;
:: original: |[
redefine func |[r]| -> Point of (TOP-REAL 1);
coherence
|[r]| is Point of (TOP-REAL 1)
proof end;
end;

theorem :: JORDAN2B:21
for r, s being Real holds s * |[r]| = |[(s * r)]| by RVSUM_1:47;

theorem :: JORDAN2B:22
for r1, r2 being Real holds |[(r1 + r2)]| = |[r1]| + |[r2]| by RVSUM_1:13;

theorem :: JORDAN2B:23
for r1, r2 being Real st |[r1]| = |[r2]| holds
r1 = r2 by FINSEQ_1:76;

theorem Th24: :: JORDAN2B:24
for P being Subset of R^1
for b being Real st P = { s where s is Real : s < b } holds
P is open
proof end;

theorem Th25: :: JORDAN2B:25
for P being Subset of R^1
for a being Real st P = { s where s is Real : a < s } holds
P is open
proof end;

theorem Th26: :: JORDAN2B:26
for P being Subset of R^1
for a, b being Real st P = { s where s is Real : ( a < s & s < b ) } holds
P is open
proof end;

theorem Th27: :: JORDAN2B:27
for u being Point of (Euclid 1)
for r, u1 being Real st <*u1*> = u holds
Ball (u,r) = { <*s*> where s is Real : ( u1 - r < s & s < u1 + r ) }
proof end;

theorem :: JORDAN2B:28
for f being Function of (TOP-REAL 1),R^1 st ( for p being Element of (TOP-REAL 1) holds f . p = p /. 1 ) holds
f is being_homeomorphism
proof end;

theorem Th29: :: JORDAN2B:29
for p being Element of (TOP-REAL 2) holds
( p /. 1 = p `1 & p /. 2 = p `2 )
proof end;

theorem :: JORDAN2B:30
for p being Element of (TOP-REAL 2) holds
( p /. 1 = proj1 . p & p /. 2 = proj2 . p )
proof end;