let n be Nat; for V being RealLinearSpace
for Kv being non void SimplicialComplex of V st n > 0 & |.Kv.| c= [#] Kv & degree Kv <= 0 holds
TopStruct(# the carrier of Kv, the topology of Kv #) = BCS (n,Kv)
let V be RealLinearSpace; for Kv being non void SimplicialComplex of V st n > 0 & |.Kv.| c= [#] Kv & degree Kv <= 0 holds
TopStruct(# the carrier of Kv, the topology of Kv #) = BCS (n,Kv)
let Kv be non void SimplicialComplex of V; ( n > 0 & |.Kv.| c= [#] Kv & degree Kv <= 0 implies TopStruct(# the carrier of Kv, the topology of Kv #) = BCS (n,Kv) )
assume that
A1:
n > 0
and
A2:
|.Kv.| c= [#] Kv
and
A3:
degree Kv <= 0
; TopStruct(# the carrier of Kv, the topology of Kv #) = BCS (n,Kv)
defpred S1[ Nat] means ( $1 > 0 implies ( TopStruct(# the carrier of Kv, the topology of Kv #) = BCS ($1,Kv) & degree (BCS ($1,Kv)) <= 0 ) );
A4:
for n being Nat st S1[n] holds
S1[n + 1]
proof
not
{} in dom (center_of_mass V)
by ZFMISC_1:56;
then A5:
dom (center_of_mass V) is
with_non-empty_elements
;
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A6:
S1[
n]
;
S1[n + 1]
assume
n + 1
> 0
;
( TopStruct(# the carrier of Kv, the topology of Kv #) = BCS ((n + 1),Kv) & degree (BCS ((n + 1),Kv)) <= 0 )
per cases
( n = 0 or n > 0 )
;
suppose A7:
n = 0
;
( TopStruct(# the carrier of Kv, the topology of Kv #) = BCS ((n + 1),Kv) & degree (BCS ((n + 1),Kv)) <= 0 )A8:
degree (subdivision ((center_of_mass V),Kv)) <= degree Kv
by A5, SIMPLEX0:52;
BCS (
(n + 1),
Kv)
= BCS Kv
by A2, A7, Th17;
hence
(
TopStruct(# the
carrier of
Kv, the
topology of
Kv #)
= BCS (
(n + 1),
Kv) &
degree (BCS ((n + 1),Kv)) <= 0 )
by A2, A3, A8, Def5, Th21;
verum end; suppose A9:
n > 0
;
( TopStruct(# the carrier of Kv, the topology of Kv #) = BCS ((n + 1),Kv) & degree (BCS ((n + 1),Kv)) <= 0 )A10:
|.Kv.| = |.(BCS (n,Kv)).|
by Th10;
[#] Kv = [#] (BCS (n,Kv))
by A6, A9;
then
BCS (
n,
Kv)
= BCS (BCS (n,Kv))
by A2, A6, A9, A10, Th21;
hence
(
TopStruct(# the
carrier of
Kv, the
topology of
Kv #)
= BCS (
(n + 1),
Kv) &
degree (BCS ((n + 1),Kv)) <= 0 )
by A2, A6, A9, Th20;
verum end; end;
end;
A11:
S1[ 0 ]
;
for n being Nat holds S1[n]
from NAT_1:sch 2(A11, A4);
hence
TopStruct(# the carrier of Kv, the topology of Kv #) = BCS (n,Kv)
by A1; verum