let V be RealLinearSpace; for Aff being finite affinely-independent Subset of V
for Sf being c=-linear finite finite-membered Subset-Family of V st Sf is with_non-empty_elements & union Sf c= Aff holds
( (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) iff for n being Nat st 0 < n & n <= card (union Sf) holds
ex x being set st
( x in Sf & card x = n ) )
let Aff be finite affinely-independent Subset of V; for Sf being c=-linear finite finite-membered Subset-Family of V st Sf is with_non-empty_elements & union Sf c= Aff holds
( (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) iff for n being Nat st 0 < n & n <= card (union Sf) holds
ex x being set st
( x in Sf & card x = n ) )
let Sf be c=-linear finite finite-membered Subset-Family of V; ( Sf is with_non-empty_elements & union Sf c= Aff implies ( (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) iff for n being Nat st 0 < n & n <= card (union Sf) holds
ex x being set st
( x in Sf & card x = n ) ) )
reconsider N = 0 as Nat ;
set U = union Sf;
assume that
A1:
Sf is with_non-empty_elements
and
A2:
union Sf c= Aff
; ( (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) iff for n being Nat st 0 < n & n <= card (union Sf) holds
ex x being set st
( x in Sf & card x = n ) )
set B = center_of_mass V;
set C = Complex_of {Aff};
reconsider s = Sf as c=-linear finite Subset-Family of (Complex_of {Aff}) ;
A3:
the topology of (Complex_of {Aff}) = bool Aff
by SIMPLEX0:4;
Segm (card (union Sf)) c= Segm (card Aff)
by A2, CARD_1:11;
then
card (union Sf) <= card Aff
by NAT_1:39;
then A4:
( N - 1 <= (card (union Sf)) - 1 & (card (union Sf)) - 1 <= (card Aff) - 1 )
by XREAL_1:9;
( Sf c= bool (union Sf) & bool (union Sf) c= bool Aff )
by A2, ZFMISC_1:67, ZFMISC_1:82;
then A5:
s c= the topology of (Complex_of {Aff})
by A3;
A6:
s is simplex-like
then A7:
card s = card ((center_of_mass V) .: Sf)
by A1, Th33;
Segm (card Sf) c= Segm (card (union Sf))
by A1, SIMPLEX0:10;
then A8:
card Sf <= card (union Sf)
by NAT_1:39;
set BC = BCS (Complex_of {Aff});
reconsider c = card Aff as ExtReal ;
A9: degree (Complex_of {Aff}) =
c - 1
by SIMPLEX0:26
.=
(card Aff) + (- 1)
by XXREAL_3:def 2
;
A10:
|.(Complex_of {Aff}).| c= [#] (Complex_of {Aff})
;
then A11:
BCS (Complex_of {Aff}) = subdivision ((center_of_mass V),(Complex_of {Aff}))
by Def5;
then
[#] (BCS (Complex_of {Aff})) = [#] (Complex_of {Aff})
by SIMPLEX0:def 20;
then reconsider BS = (center_of_mass V) .: Sf as Subset of (BCS (Complex_of {Aff})) ;
A12:
N - 1 <= (card Aff) - 1
by XREAL_1:9;
A13:
degree (BCS (Complex_of {Aff})) = degree (Complex_of {Aff})
by A10, Th31;
thus
( (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) implies for n being Nat st 0 < n & n <= card (union Sf) holds
ex x being set st
( x in Sf & card x = n ) )
( ( for n being Nat st 0 < n & n <= card (union Sf) holds
ex x being set st
( x in Sf & card x = n ) ) implies (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) )proof
assume
(center_of_mass V) .: Sf is
Simplex of
(card (union Sf)) - 1,
BCS (Complex_of {Aff})
;
for n being Nat st 0 < n & n <= card (union Sf) holds
ex x being set st
( x in Sf & card x = n )
then reconsider BS =
(center_of_mass V) .: Sf as
Simplex of
(card (union Sf)) - 1,
BCS (Complex_of {Aff}) ;
reconsider c1 =
(card (union Sf)) - 1 as
ExtReal ;
let n be
Nat;
( 0 < n & n <= card (union Sf) implies ex x being set st
( x in Sf & card x = n ) )
reconsider s =
Sf as
Subset-Family of
(union Sf) by ZFMISC_1:82;
defpred S1[
Nat]
means ( $1
< card Sf implies ex
x being
finite set st
(
x in Sf &
card x = (card Sf) - $1 ) );
assume that A14:
0 < n
and A15:
n <= card (union Sf)
;
ex x being set st
( x in Sf & card x = n )
A16:
(card Sf) - 0 > (card Sf) - n
by A14, XREAL_1:10;
A17:
card BS =
c1 + 1
by A4, A9, A13, SIMPLEX0:def 18
.=
((card (union Sf)) - 1) + 1
by XXREAL_3:def 2
.=
card (union Sf)
;
then A18:
not
Sf is
empty
by A14, A15;
then consider s1 being
Subset-Family of
(union Sf) such that A19:
s c= s1
and
(
s1 is
with_non-empty_elements &
s1 is
c=-linear )
and A20:
card (union Sf) = card s1
and A21:
for
Z being
set st
Z in s1 &
card Z <> 1 holds
ex
x being
set st
(
x in Z &
Z \ {x} in s1 )
by A1, SIMPLEX0:9, SIMPLEX0:13;
card (union Sf) = card Sf
by A1, A6, A17, Th33;
then A22:
s = s1
by A19, A20, CARD_2:102;
A23:
for
n being
Nat st
S1[
n] holds
S1[
n + 1]
A30:
S1[
0 ]
by A7, A17, A18, SIMPLEX0:9;
A31:
for
n being
Nat holds
S1[
n]
from NAT_1:sch 2(A30, A23);
(card Sf) - n is
Nat
by A7, A15, A17, NAT_1:21;
then
ex
x being
finite set st
(
x in Sf &
card x = (card Sf) - ((card Sf) - n) )
by A16, A31;
hence
ex
x being
set st
(
x in Sf &
card x = n )
;
verum
end;
assume A32:
for n being Nat st 0 < n & n <= card (union Sf) holds
ex x being set st
( x in Sf & card x = n )
; (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff})
per cases
( union Sf is empty or not union Sf is empty )
;
suppose A36:
not
union Sf is
empty
;
(center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff})reconsider c1 =
(card (union Sf)) - 1 as
ExtReal ;
consider x being
set such that A37:
x in Sf
and
card x = card (union Sf)
by A32, A36;
defpred S1[
object ,
object ]
means ex
D2 being
set st
(
D2 = $2 &
card D2 = $1 );
A38:
for
x being
object st
x in Seg (card (union Sf)) holds
ex
y being
object st
(
y in Sf &
S1[
x,
y] )
consider f being
Function of
(Seg (card (union Sf))),
Sf such that A40:
for
x being
object st
x in Seg (card (union Sf)) holds
S1[
x,
f . x]
from FUNCT_2:sch 1(A38);
then A44:
(
rng f c= Sf &
f is
one-to-one )
by FUNCT_1:def 4;
dom f = Seg (card (union Sf))
by A37, FUNCT_2:def 1;
then
(
Segm (card (Seg (card (union Sf)))) = Segm (card (union Sf)) &
Segm (card (Seg (card (union Sf)))) c= Segm (card Sf) )
by A44, CARD_1:10, FINSEQ_1:57;
then
card (union Sf) <= card Sf
by NAT_1:39;
then A45:
card BS = card (union Sf)
by A7, A8, XXREAL_0:1;
(
BS is
Simplex of
(BCS (Complex_of {Aff})) &
c1 + 1
= ((card (union Sf)) - 1) + 1 )
by A6, A11, SIMPLEX0:def 20, XXREAL_3:def 2;
hence
(center_of_mass V) .: Sf is
Simplex of
(card (union Sf)) - 1,
BCS (Complex_of {Aff})
by A4, A9, A13, A45, SIMPLEX0:def 18;
verum end; end;