:: Projections in n-Dimensional Euclidean Space to Each Coordinates
:: by Roman Matuszewski and Yatsuka Nakamura
::
:: Received November 3, 1997
:: Copyright (c) 1997 Association of Mizar Users
Lm1:
for n, i being Element of 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 )
Lm2:
for n, i being Element of NAT
for p being Element of (TOP-REAL n) ex q being Real st
for g being FinSequence of REAL st g = p holds
q = g /. i
:: deftheorem Def1 defines Proj JORDAN2B:def 1 :
theorem :: JORDAN2B:1
theorem :: JORDAN2B:2
canceled;
theorem :: JORDAN2B:3
theorem :: JORDAN2B:4
theorem :: JORDAN2B:5
theorem :: JORDAN2B:6
theorem Th7: :: JORDAN2B:7
theorem :: JORDAN2B:8
canceled;
theorem Th9: :: JORDAN2B:9
theorem Th10: :: JORDAN2B:10
theorem Th11: :: JORDAN2B:11
theorem :: JORDAN2B:12
theorem :: JORDAN2B:13
theorem Th14: :: JORDAN2B:14
theorem Th15: :: JORDAN2B:15
theorem Th16: :: JORDAN2B:16
theorem Th17: :: JORDAN2B:17
theorem Th18: :: JORDAN2B:18
theorem Th19: :: JORDAN2B:19
theorem Th20: :: JORDAN2B:20
theorem Th21: :: JORDAN2B:21
theorem Th22: :: JORDAN2B:22
theorem :: JORDAN2B:23
theorem Th24: :: JORDAN2B:24
theorem :: JORDAN2B:25
canceled;
theorem :: JORDAN2B:26
theorem :: JORDAN2B:27
theorem :: JORDAN2B:28
canceled;
theorem :: JORDAN2B:29
theorem Th30: :: JORDAN2B:30
theorem Th31: :: JORDAN2B:31
theorem Th32: :: JORDAN2B:32
theorem Th33: :: JORDAN2B:33
theorem :: JORDAN2B:34
theorem Th35: :: JORDAN2B:35
theorem :: JORDAN2B:36