:: by Karol P\kak

::

:: Received December 21, 2010

:: Copyright (c) 2010-2019 Association of Mizar Users

Lm1: for n being Nat

for f being b

proof end;

theorem Th1: :: RLAFFIN3:1

for f1, f2 being real-valued FinSequence

for r being Real holds (Intervals (f1,r)) ^ (Intervals (f2,r)) = Intervals ((f1 ^ f2),r)

for r being Real holds (Intervals (f1,r)) ^ (Intervals (f2,r)) = Intervals ((f1 ^ f2),r)

proof end;

theorem Th2: :: RLAFFIN3:2

for x being set

for f1, f2 being FinSequence holds

( x in product (f1 ^ f2) iff ex p1, p2 being FinSequence st

( x = p1 ^ p2 & p1 in product f1 & p2 in product f2 ) )

for f1, f2 being FinSequence holds

( x in product (f1 ^ f2) iff ex p1, p2 being FinSequence st

( x = p1 ^ p2 & p1 in product f1 & p2 in product f2 ) )

proof end;

Lm2: for V being RealLinearSpace

for A being Subset of V holds Lin A = Lin (A \ {(0. V)})

proof end;

registration

let V be finite-dimensional RealLinearSpace;

coherence

for b_{1} being affinely-independent Subset of V holds b_{1} is finite

end;
coherence

for b

proof end;

registration

let n be Nat;

coherence

( TOP-REAL n is add-continuous & TOP-REAL n is Mult-continuous )

TOP-REAL n is finite-dimensional

end;
coherence

( TOP-REAL n is add-continuous & TOP-REAL n is Mult-continuous )

proof end;

coherence TOP-REAL n is finite-dimensional

proof end;

theorem Th5: :: RLAFFIN3:5

for V being finite-dimensional RealLinearSpace

for A being affinely-independent Subset of V holds card A <= 1 + (dim V)

for A being affinely-independent Subset of V holds card A <= 1 + (dim V)

proof end;

theorem Th6: :: RLAFFIN3:6

for V being finite-dimensional RealLinearSpace

for A being affinely-independent Subset of V holds

( card A = (dim V) + 1 iff Affin A = [#] V )

for A being affinely-independent Subset of V holds

( card A = (dim V) + 1 iff Affin A = [#] V )

proof end;

:: Space

theorem Th7: :: RLAFFIN3:7

for n, k being Nat

for An being Subset of (TOP-REAL n)

for Ak being Subset of (TOP-REAL k) st k <= n & An = { v where v is Element of (TOP-REAL n) : v | k in Ak } holds

( An is open iff Ak is open )

for An being Subset of (TOP-REAL n)

for Ak being Subset of (TOP-REAL k) st k <= n & An = { v where v is Element of (TOP-REAL n) : v | k in Ak } holds

( An is open iff Ak is open )

proof end;

Lm3: for n being Nat holds the carrier of (n -VectSp_over F_Real) = the carrier of (TOP-REAL n)

proof end;

theorem Th8: :: RLAFFIN3:8

for n, k being Nat

for Ak being Subset of (TOP-REAL k)

for A being Subset of (TOP-REAL (k + n)) st A = { (v ^ (n |-> 0)) where v is Element of (TOP-REAL k) : verum } holds

for B being Subset of ((TOP-REAL (k + n)) | A) st B = { v where v is Point of (TOP-REAL (k + n)) : ( v | k in Ak & v in A ) } holds

( Ak is open iff B is open )

for Ak being Subset of (TOP-REAL k)

for A being Subset of (TOP-REAL (k + n)) st A = { (v ^ (n |-> 0)) where v is Element of (TOP-REAL k) : verum } holds

for B being Subset of ((TOP-REAL (k + n)) | A) st B = { v where v is Point of (TOP-REAL (k + n)) : ( v | k in Ak & v in A ) } holds

( Ak is open iff B is open )

proof end;

theorem Th9: :: RLAFFIN3:9

for V being RealLinearSpace

for A being affinely-independent Subset of V

for B being Subset of V st B c= A holds

(conv A) /\ (Affin B) = conv B

for A being affinely-independent Subset of V

for B being Subset of V st B c= A holds

(conv A) /\ (Affin B) = conv B

proof end;

theorem Th10: :: RLAFFIN3:10

for r being Real

for V being non empty RLSStruct

for A being non empty set

for f being PartFunc of A, the carrier of V

for X being set holds (r (#) f) .: X = r * (f .: X)

for V being non empty RLSStruct

for A being non empty set

for f being PartFunc of A, the carrier of V

for X being set holds (r (#) f) .: X = r * (f .: X)

proof end;

registration

let V be non empty addLoopStr ;

let A be finite Subset of V;

let v be Element of V;

coherence

v + A is finite

end;
let A be finite Subset of V;

let v be Element of V;

coherence

v + A is finite

proof end;

Lm4: for V being non empty RLSStruct

for A being Subset of V

for r being Real holds card (r * A) c= card A

proof end;

registration

let V be non empty RLSStruct ;

let A be finite Subset of V;

let r be Real;

coherence

r * A is finite

end;
let A be finite Subset of V;

let r be Real;

coherence

r * A is finite

proof end;

theorem Th12: :: RLAFFIN3:12

for r being Real

for V being RealLinearSpace

for A being Subset of V holds

( card A = card (r * A) iff ( r <> 0 or A is trivial ) )

for V being RealLinearSpace

for A being Subset of V holds

( card A = card (r * A) iff ( r <> 0 or A is trivial ) )

proof end;

registration

let V be non empty RLSStruct ;

let f be FinSequence of V;

let r be Real;

coherence

r (#) f is FinSequence-like

end;
let f be FinSequence of V;

let r be Real;

coherence

r (#) f is FinSequence-like

proof end;

definition
end;

:: deftheorem Def1 defines Enumeration RLAFFIN3:def 1 :

for X being finite set

for b_{2} being one-to-one FinSequence holds

( b_{2} is Enumeration of X iff rng b_{2} = X );

for X being finite set

for b

( b

definition

let X be set ;

let A be finite Subset of X;

:: original: Enumeration

redefine mode Enumeration of A -> one-to-one FinSequence of X;

coherence

for b_{1} being Enumeration of A holds b_{1} is one-to-one FinSequence of X

end;
let A be finite Subset of X;

:: original: Enumeration

redefine mode Enumeration of A -> one-to-one FinSequence of X;

coherence

for b

proof end;

theorem Th13: :: RLAFFIN3:13

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for A being finite Subset of V

for E being Enumeration of A

for v being Element of V holds E + ((card A) |-> v) is Enumeration of v + A

for A being finite Subset of V

for E being Enumeration of A

for v being Element of V holds E + ((card A) |-> v) is Enumeration of v + A

proof end;

theorem :: RLAFFIN3:14

for r being Real

for V being RealLinearSpace

for Av being finite Subset of V

for E being Enumeration of Av holds

( r (#) E is Enumeration of r * Av iff ( r <> 0 or Av is trivial ) )

for V being RealLinearSpace

for Av being finite Subset of V

for E being Enumeration of Av holds

( r (#) E is Enumeration of r * Av iff ( r <> 0 or Av is trivial ) )

proof end;

theorem Th15: :: RLAFFIN3:15

for n, m being Nat

for M being Matrix of n,m,F_Real st the_rank_of M = n holds

for A being finite Subset of (TOP-REAL n)

for E being Enumeration of A holds (Mx2Tran M) * E is Enumeration of (Mx2Tran M) .: A

for M being Matrix of n,m,F_Real st the_rank_of M = n holds

for A being finite Subset of (TOP-REAL n)

for E being Enumeration of A holds (Mx2Tran M) * E is Enumeration of (Mx2Tran M) .: A

proof end;

definition

let V be RealLinearSpace;

let Av be finite Subset of V;

let E be Enumeration of Av;

let x be object ;

coherence

(x |-- Av) * E is FinSequence of REAL ;

end;
let Av be finite Subset of V;

let E be Enumeration of Av;

let x be object ;

coherence

(x |-- Av) * E is FinSequence of REAL ;

:: deftheorem defines |-- RLAFFIN3:def 2 :

for V being RealLinearSpace

for Av being finite Subset of V

for E being Enumeration of Av

for x being object holds x |-- E = (x |-- Av) * E;

for V being RealLinearSpace

for Av being finite Subset of V

for E being Enumeration of Av

for x being object holds x |-- E = (x |-- Av) * E;

theorem Th16: :: RLAFFIN3:16

for V being RealLinearSpace

for Av being finite Subset of V

for x being object

for E being Enumeration of Av holds len (x |-- E) = card Av

for Av being finite Subset of V

for x being object

for E being Enumeration of Av holds len (x |-- E) = card Av

proof end;

theorem Th17: :: RLAFFIN3:17

for V being RealLinearSpace

for v, w being VECTOR of V

for Affv being finite affinely-independent Subset of V

for EV being Enumeration of Affv

for E being Enumeration of v + Affv st w in Affin Affv & E = EV + ((card Affv) |-> v) holds

w |-- EV = (v + w) |-- E

for v, w being VECTOR of V

for Affv being finite affinely-independent Subset of V

for EV being Enumeration of Affv

for E being Enumeration of v + Affv st w in Affin Affv & E = EV + ((card Affv) |-> v) holds

w |-- EV = (v + w) |-- E

proof end;

theorem :: RLAFFIN3:18

for r being Real

for V being RealLinearSpace

for v being VECTOR of V

for Affv being finite affinely-independent Subset of V

for EV being Enumeration of Affv

for rE being Enumeration of r * Affv st v in Affin Affv & rE = r (#) EV & r <> 0 holds

v |-- EV = (r * v) |-- rE

for V being RealLinearSpace

for v being VECTOR of V

for Affv being finite affinely-independent Subset of V

for EV being Enumeration of Affv

for rE being Enumeration of r * Affv st v in Affin Affv & rE = r (#) EV & r <> 0 holds

v |-- EV = (r * v) |-- rE

proof end;

theorem Th19: :: RLAFFIN3:19

for n, m being Nat

for Affn being affinely-independent Subset of (TOP-REAL n)

for EN being Enumeration of Affn

for M being Matrix of n,m,F_Real st the_rank_of M = n holds

for ME being Enumeration of (Mx2Tran M) .: Affn st ME = (Mx2Tran M) * EN holds

for pn being Point of (TOP-REAL n) st pn in Affin Affn holds

pn |-- EN = ((Mx2Tran M) . pn) |-- ME

for Affn being affinely-independent Subset of (TOP-REAL n)

for EN being Enumeration of Affn

for M being Matrix of n,m,F_Real st the_rank_of M = n holds

for ME being Enumeration of (Mx2Tran M) .: Affn st ME = (Mx2Tran M) * EN holds

for pn being Point of (TOP-REAL n) st pn in Affin Affn holds

pn |-- EN = ((Mx2Tran M) . pn) |-- ME

proof end;

theorem Th20: :: RLAFFIN3:20

for x being set

for V being RealLinearSpace

for Affv being finite affinely-independent Subset of V

for EV being Enumeration of Affv

for A being Subset of V st A c= Affv & x in Affin Affv holds

( x in Affin A iff for y being set st y in dom (x |-- EV) & not EV . y in A holds

(x |-- EV) . y = 0 )

for V being RealLinearSpace

for Affv being finite affinely-independent Subset of V

for EV being Enumeration of Affv

for A being Subset of V st A c= Affv & x in Affin Affv holds

( x in Affin A iff for y being set st y in dom (x |-- EV) & not EV . y in A holds

(x |-- EV) . y = 0 )

proof end;

theorem :: RLAFFIN3:21

for x being set

for k being Nat

for V being RealLinearSpace

for Affv being finite affinely-independent Subset of V

for EV being Enumeration of Affv st x in Affin Affv holds

( x in Affin (EV .: (Seg k)) iff x |-- EV = ((x |-- EV) | k) ^ (((card Affv) -' k) |-> 0) )

for k being Nat

for V being RealLinearSpace

for Affv being finite affinely-independent Subset of V

for EV being Enumeration of Affv st x in Affin Affv holds

( x in Affin (EV .: (Seg k)) iff x |-- EV = ((x |-- EV) | k) ^ (((card Affv) -' k) |-> 0) )

proof end;

theorem Th22: :: RLAFFIN3:22

for x being set

for k being Nat

for V being RealLinearSpace

for Affv being finite affinely-independent Subset of V

for EV being Enumeration of Affv st k <= card Affv & x in Affin Affv holds

( x in Affin (Affv \ (EV .: (Seg k))) iff x |-- EV = (k |-> 0) ^ ((x |-- EV) /^ k) )

for k being Nat

for V being RealLinearSpace

for Affv being finite affinely-independent Subset of V

for EV being Enumeration of Affv st k <= card Affv & x in Affin Affv holds

( x in Affin (Affv \ (EV .: (Seg k))) iff x |-- EV = (k |-> 0) ^ ((x |-- EV) /^ k) )

proof end;

theorem Th23: :: RLAFFIN3:23

for n being Nat

for Affn being affinely-independent Subset of (TOP-REAL n)

for EN being Enumeration of Affn st 0* n in Affn & EN . (len EN) = 0* n holds

( rng (EN | ((card Affn) -' 1)) = Affn \ {(0* n)} & ( for A being Subset of (n -VectSp_over F_Real) st Affn = A holds

EN | ((card Affn) -' 1) is OrdBasis of Lin A ) )

for Affn being affinely-independent Subset of (TOP-REAL n)

for EN being Enumeration of Affn st 0* n in Affn & EN . (len EN) = 0* n holds

( rng (EN | ((card Affn) -' 1)) = Affn \ {(0* n)} & ( for A being Subset of (n -VectSp_over F_Real) st Affn = A holds

EN | ((card Affn) -' 1) is OrdBasis of Lin A ) )

proof end;

Lm5: 0 in REAL

by XREAL_0:def 1;

theorem Th24: :: RLAFFIN3:24

for n being Nat

for Affn being affinely-independent Subset of (TOP-REAL n)

for EN being Enumeration of Affn

for A being Subset of (n -VectSp_over F_Real) st Affn = A & 0* n in Affn & EN . (len EN) = 0* n holds

for B being OrdBasis of Lin A st B = EN | ((card Affn) -' 1) holds

for v being Element of (Lin A) holds v |-- B = (v |-- EN) | ((card Affn) -' 1)

for Affn being affinely-independent Subset of (TOP-REAL n)

for EN being Enumeration of Affn

for A being Subset of (n -VectSp_over F_Real) st Affn = A & 0* n in Affn & EN . (len EN) = 0* n holds

for B being OrdBasis of Lin A st B = EN | ((card Affn) -' 1) holds

for v being Element of (Lin A) holds v |-- B = (v |-- EN) | ((card Affn) -' 1)

proof end;

Lm6: for k being Nat

for V being LinearTopSpace

for A being finite affinely-independent Subset of V

for E being Enumeration of A

for v being Point of V

for Ev being Enumeration of v + A st Ev = E + ((card A) |-> v) holds

for X being set holds (transl (v,V)) .: { u where u is Point of V : ( u in Affin A & (u |-- E) | k in X ) } = { w where w is Point of V : ( w in Affin (v + A) & (w |-- Ev) | k in X ) }

proof end;

Lm7: for n, k being Nat st k <= n holds

for A being non empty finite affinely-independent Subset of (TOP-REAL n) st card A = n + 1 holds

for E being Enumeration of A st E . (len E) = 0* n holds

for P being Subset of (TOP-REAL k)

for B being Subset of (TOP-REAL n) st B = { pn where pn is Point of (TOP-REAL n) : (pn |-- E) | k in P } holds

( P is open iff B is open )

proof end;

Lm8: for n, k being Nat

for A being non empty finite affinely-independent Subset of (TOP-REAL n) st k < card A holds

for E being Enumeration of A st E . (len E) = 0* n holds

for P being Subset of (TOP-REAL k)

for B being Subset of ((TOP-REAL n) | (Affin A)) st B = { v where v is Element of ((TOP-REAL n) | (Affin A)) : (v |-- E) | k in P } holds

( P is open iff B is open )

proof end;

theorem Th25: :: RLAFFIN3:25

for n, k being Nat

for Affn being affinely-independent Subset of (TOP-REAL n)

for Ak being Subset of (TOP-REAL k)

for EN being Enumeration of Affn

for An being Subset of (TOP-REAL n) st k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } holds

( Ak is open iff An is open )

for Affn being affinely-independent Subset of (TOP-REAL n)

for Ak being Subset of (TOP-REAL k)

for EN being Enumeration of Affn

for An being Subset of (TOP-REAL n) st k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } holds

( Ak is open iff An is open )

proof end;

theorem Th26: :: RLAFFIN3:26

for n, k being Nat

for An being Subset of (TOP-REAL n)

for Affn being affinely-independent Subset of (TOP-REAL n)

for Ak being Subset of (TOP-REAL k)

for EN being Enumeration of Affn st k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } holds

( Ak is closed iff An is closed )

for An being Subset of (TOP-REAL n)

for Affn being affinely-independent Subset of (TOP-REAL n)

for Ak being Subset of (TOP-REAL k)

for EN being Enumeration of Affn st k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } holds

( Ak is closed iff An is closed )

proof end;

registration

let n be Nat;

coherence

for b_{1} being Subset of (TOP-REAL n) st b_{1} is Affine holds

b_{1} is closed

end;
coherence

for b

b

proof end;

theorem Th27: :: RLAFFIN3:27

for n, k being Nat

for Affn being affinely-independent Subset of (TOP-REAL n)

for Ak being Subset of (TOP-REAL k)

for EN being Enumeration of Affn

for B being Subset of ((TOP-REAL n) | (Affin Affn)) st k < card Affn & B = { pnA where pnA is Element of ((TOP-REAL n) | (Affin Affn)) : (pnA |-- EN) | k in Ak } holds

( Ak is open iff B is open )

for Affn being affinely-independent Subset of (TOP-REAL n)

for Ak being Subset of (TOP-REAL k)

for EN being Enumeration of Affn

for B being Subset of ((TOP-REAL n) | (Affin Affn)) st k < card Affn & B = { pnA where pnA is Element of ((TOP-REAL n) | (Affin Affn)) : (pnA |-- EN) | k in Ak } holds

( Ak is open iff B is open )

proof end;

theorem Th28: :: RLAFFIN3:28

for n, k being Nat

for Affn being affinely-independent Subset of (TOP-REAL n)

for Ak being Subset of (TOP-REAL k)

for EN being Enumeration of Affn

for B being Subset of ((TOP-REAL n) | (Affin Affn)) st k < card Affn & B = { pnA where pnA is Element of ((TOP-REAL n) | (Affin Affn)) : (pnA |-- EN) | k in Ak } holds

( Ak is closed iff B is closed )

for Affn being affinely-independent Subset of (TOP-REAL n)

for Ak being Subset of (TOP-REAL k)

for EN being Enumeration of Affn

for B being Subset of ((TOP-REAL n) | (Affin Affn)) st k < card Affn & B = { pnA where pnA is Element of ((TOP-REAL n) | (Affin Affn)) : (pnA |-- EN) | k in Ak } holds

( Ak is closed iff B is closed )

proof end;

registration
end;

definition

let V be RealLinearSpace;

let A be Subset of V;

let x be set ;

ex b_{1} being Function of V,R^1 st

for v being VECTOR of V holds b_{1} . v = (v |-- A) . x

for b_{1}, b_{2} being Function of V,R^1 st ( for v being VECTOR of V holds b_{1} . v = (v |-- A) . x ) & ( for v being VECTOR of V holds b_{2} . v = (v |-- A) . x ) holds

b_{1} = b_{2}

end;
let A be Subset of V;

let x be set ;

func |-- (A,x) -> Function of V,R^1 means :Def3: :: RLAFFIN3:def 3

for v being VECTOR of V holds it . v = (v |-- A) . x;

existence for v being VECTOR of V holds it . v = (v |-- A) . x;

ex b

for v being VECTOR of V holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines |-- RLAFFIN3:def 3 :

for V being RealLinearSpace

for A being Subset of V

for x being set

for b_{4} being Function of V,R^1 holds

( b_{4} = |-- (A,x) iff for v being VECTOR of V holds b_{4} . v = (v |-- A) . x );

for V being RealLinearSpace

for A being Subset of V

for x being set

for b

( b

theorem Th29: :: RLAFFIN3:29

for x being set

for V being RealLinearSpace

for A being Subset of V st not x in A holds

|-- (A,x) = ([#] V) --> 0

for V being RealLinearSpace

for A being Subset of V st not x in A holds

|-- (A,x) = ([#] V) --> 0

proof end;

theorem :: RLAFFIN3:30

for x being set

for V being RealLinearSpace

for A being affinely-independent Subset of V st |-- (A,x) = ([#] V) --> 0 holds

not x in A

for V being RealLinearSpace

for A being affinely-independent Subset of V st |-- (A,x) = ([#] V) --> 0 holds

not x in A

proof end;

theorem Th31: :: RLAFFIN3:31

for x being set

for n being Nat

for Affn being affinely-independent Subset of (TOP-REAL n) holds (|-- (Affn,x)) | (Affin Affn) is continuous Function of ((TOP-REAL n) | (Affin Affn)),R^1

for n being Nat

for Affn being affinely-independent Subset of (TOP-REAL n) holds (|-- (Affn,x)) | (Affin Affn) is continuous Function of ((TOP-REAL n) | (Affin Affn)),R^1

proof end;

theorem Th32: :: RLAFFIN3:32

for x being set

for n being Nat

for Affn being affinely-independent Subset of (TOP-REAL n) st card Affn = n + 1 holds

|-- (Affn,x) is continuous

for n being Nat

for Affn being affinely-independent Subset of (TOP-REAL n) st card Affn = n + 1 holds

|-- (Affn,x) is continuous

proof end;

Lm9: for n being Nat

for A being affinely-independent Subset of (TOP-REAL n) st card A = n + 1 holds

conv A is closed

proof end;

registration

let n be Nat;

let Affn be affinely-independent Subset of (TOP-REAL n);

coherence

conv Affn is closed

end;
let Affn be affinely-independent Subset of (TOP-REAL n);

coherence

conv Affn is closed

proof end;

theorem :: RLAFFIN3:33

for n being Nat

for Affn being affinely-independent Subset of (TOP-REAL n) st card Affn = n + 1 holds

Int Affn is open

for Affn being affinely-independent Subset of (TOP-REAL n) st card Affn = n + 1 holds

Int Affn is open

proof end;