let V be RealLinearSpace; for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv & degree Kv <= 0 holds
TopStruct(# the carrier of Kv, the topology of Kv #) = BCS Kv
let Kv be non void SimplicialComplex of V; ( |.Kv.| c= [#] Kv & degree Kv <= 0 implies TopStruct(# the carrier of Kv, the topology of Kv #) = BCS Kv )
reconsider o = 1 as ExtReal ;
assume that
A1:
|.Kv.| c= [#] Kv
and
A2:
degree Kv <= 0
; TopStruct(# the carrier of Kv, the topology of Kv #) = BCS Kv
set B = center_of_mass V;
set BC = BCS Kv;
A3:
BCS Kv = subdivision ((center_of_mass V),Kv)
by A1, Def5;
then A4:
[#] (BCS Kv) = [#] Kv
by SIMPLEX0:def 20;
A5:
dom (center_of_mass V) = (bool the carrier of V) \ {{}}
by FUNCT_2:def 1;
A6:
( 0 + o = 0 + 1 & (degree Kv) + o <= 0 + o )
by A2, XXREAL_3:35, XXREAL_3:def 2;
A7:
the topology of (BCS Kv) c= the topology of Kv
proof
let x be
object ;
TARSKI:def 3 ( not x in the topology of (BCS Kv) or x in the topology of Kv )
assume
x in the
topology of
(BCS Kv)
;
x in the topology of Kv
then reconsider X =
x as
Simplex of
(BCS Kv) by PRE_TOPC:def 2;
reconsider X1 =
X as
Subset of
Kv by A4;
consider S being
c=-linear finite simplex-like Subset-Family of
Kv such that A8:
X = (center_of_mass V) .: S
by A3, SIMPLEX0:def 20;
A9:
(center_of_mass V) .: S = (center_of_mass V) .: (S /\ (dom (center_of_mass V)))
by RELAT_1:112;
per cases
( X is empty or not X is empty )
;
suppose A10:
not
X is
empty
;
x in the topology of Kvthen
not
S is
empty
by A8;
then
union S in S
by SIMPLEX0:9;
then reconsider U =
union S as
Simplex of
Kv by TOPS_2:def 1;
A11:
not
U is
empty
then A15:
@ U in dom (center_of_mass V)
by A5, ZFMISC_1:56;
card U <= (degree Kv) + 1
by SIMPLEX0:24;
then A16:
card U <= 1
by A6, XXREAL_0:2;
card U >= 1
by A11, NAT_1:14;
then A17:
card U = 1
by A16, XXREAL_0:1;
then consider u being
object such that A18:
{u} = @ U
by CARD_2:42;
u in {u}
by TARSKI:def 1;
then reconsider u =
u as
Element of
V by A18;
A19:
S /\ (dom (center_of_mass V)) c= {U}
not
S /\ (dom (center_of_mass V)) is
empty
by A8, A9, A10;
then
S /\ (dom (center_of_mass V)) = {U}
by A19, ZFMISC_1:33;
then X =
Im (
(center_of_mass V),
U)
by A8, A9, RELAT_1:def 16
.=
{((center_of_mass V) . U)}
by A15, FUNCT_1:59
.=
{((1 / 1) * (Sum {u}))}
by A17, A18, RLAFFIN2:def 2
.=
{(Sum {u})}
by RLVECT_1:def 8
.=
U
by A18, RLVECT_2:9
;
hence
x in the
topology of
Kv
by PRE_TOPC:def 2;
verum end;
end;
the topology of Kv c= the topology of (BCS Kv)
proof
let x be
object ;
TARSKI:def 3 ( not x in the topology of Kv or x in the topology of (BCS Kv) )
assume
x in the
topology of
Kv
;
x in the topology of (BCS Kv)
then reconsider X =
x as
Simplex of
Kv by PRE_TOPC:def 2;
reconsider X1 =
X as
Subset of
(BCS Kv) by A4;
per cases
( X is empty or not X is empty )
;
suppose A22:
not
X is
empty
;
x in the topology of (BCS Kv)
for
Y being
Subset of
Kv st
Y in {X} holds
Y is
simplex-like
by TARSKI:def 1;
then reconsider XX =
{X} as
finite simplex-like Subset-Family of
Kv by TOPS_2:def 1;
then A25:
XX is
c=-linear
;
card X <= (degree Kv) + 1
by SIMPLEX0:24;
then A26:
card X <= 1
by A6, XXREAL_0:2;
card X >= 1
by A22, NAT_1:14;
then A27:
card X = 1
by A26, XXREAL_0:1;
then consider u being
object such that A28:
@ X = {u}
by CARD_2:42;
A29:
@ X in dom (center_of_mass V)
by A5, A22, ZFMISC_1:56;
u in {u}
by TARSKI:def 1;
then reconsider u =
u as
Element of
V by A28;
(center_of_mass V) .: XX =
Im (
(center_of_mass V),
X)
by RELAT_1:def 16
.=
{((center_of_mass V) . X)}
by A29, FUNCT_1:59
.=
{((1 / 1) * (Sum {u}))}
by A27, A28, RLAFFIN2:def 2
.=
{(Sum {u})}
by RLVECT_1:def 8
.=
X1
by A28, RLVECT_2:9
;
then
X1 is
simplex-like
by A3, A25, SIMPLEX0:def 20;
hence
x in the
topology of
(BCS Kv)
;
verum
end;
hence
TopStruct(# the carrier of Kv, the topology of Kv #) = BCS Kv
by A3, A4, A7, XBOOLE_0:def 10; verum