let X be set ; for n, k being Nat
for V being RealLinearSpace
for Aff being finite affinely-independent Subset of V
for S being Simplex of n - 1, BCS (k,(Complex_of {Aff})) st card Aff = n + 1 & X = { S1 where S1 is Simplex of n, BCS (k,(Complex_of {Aff})) : S c= S1 } holds
( ( conv (@ S) meets Int Aff implies card X = 2 ) & ( conv (@ S) misses Int Aff implies card X = 1 ) )
let n, k be Nat; for V being RealLinearSpace
for Aff being finite affinely-independent Subset of V
for S being Simplex of n - 1, BCS (k,(Complex_of {Aff})) st card Aff = n + 1 & X = { S1 where S1 is Simplex of n, BCS (k,(Complex_of {Aff})) : S c= S1 } holds
( ( conv (@ S) meets Int Aff implies card X = 2 ) & ( conv (@ S) misses Int Aff implies card X = 1 ) )
let V be RealLinearSpace; for Aff being finite affinely-independent Subset of V
for S being Simplex of n - 1, BCS (k,(Complex_of {Aff})) st card Aff = n + 1 & X = { S1 where S1 is Simplex of n, BCS (k,(Complex_of {Aff})) : S c= S1 } holds
( ( conv (@ S) meets Int Aff implies card X = 2 ) & ( conv (@ S) misses Int Aff implies card X = 1 ) )
let Aff be finite affinely-independent Subset of V; for S being Simplex of n - 1, BCS (k,(Complex_of {Aff})) st card Aff = n + 1 & X = { S1 where S1 is Simplex of n, BCS (k,(Complex_of {Aff})) : S c= S1 } holds
( ( conv (@ S) meets Int Aff implies card X = 2 ) & ( conv (@ S) misses Int Aff implies card X = 1 ) )
let S be Simplex of n - 1, BCS (k,(Complex_of {Aff})); ( card Aff = n + 1 & X = { S1 where S1 is Simplex of n, BCS (k,(Complex_of {Aff})) : S c= S1 } implies ( ( conv (@ S) meets Int Aff implies card X = 2 ) & ( conv (@ S) misses Int Aff implies card X = 1 ) ) )
assume A1:
card Aff = n + 1
; ( not X = { S1 where S1 is Simplex of n, BCS (k,(Complex_of {Aff})) : S c= S1 } or ( ( conv (@ S) meets Int Aff implies card X = 2 ) & ( conv (@ S) misses Int Aff implies card X = 1 ) ) )
set C = Complex_of {Aff};
reconsider cA = card Aff as ExtReal ;
A2: cA - 1 =
(card Aff) + (- 1)
by XXREAL_3:def 2
.=
n
by A1
;
then A3:
degree (Complex_of {Aff}) = n
by SIMPLEX0:26;
defpred S1[ Nat] means for S being Simplex of n - 1, BCS ($1,(Complex_of {Aff}))
for X being set st X = { S1 where S1 is Simplex of n, BCS ($1,(Complex_of {Aff})) : S c= S1 } holds
( ( conv (@ S) meets Int Aff implies card X = 2 ) & ( conv (@ S) misses Int Aff implies card X = 1 ) );
A4:
( [#] (Complex_of {Aff}) = [#] V & |.(Complex_of {Aff}).| c= [#] V )
;
A5:
S1[ 0 ]
proof
reconsider n1 =
n - 1 as
ExtReal ;
A6:
the
topology of
(Complex_of {Aff}) = bool Aff
by SIMPLEX0:4;
Aff in bool Aff
by ZFMISC_1:def 1;
then reconsider A1 =
Aff as
finite Simplex of
(Complex_of {Aff}) by A6, PRE_TOPC:def 2;
A7:
BCS (
0,
(Complex_of {Aff}))
= Complex_of {Aff}
by A4, Th16;
let S be
Simplex of
n - 1,
BCS (
0,
(Complex_of {Aff}));
for X being set st X = { S1 where S1 is Simplex of n, BCS (0,(Complex_of {Aff})) : S c= S1 } holds
( ( conv (@ S) meets Int Aff implies card X = 2 ) & ( conv (@ S) misses Int Aff implies card X = 1 ) )let X be
set ;
( X = { S1 where S1 is Simplex of n, BCS (0,(Complex_of {Aff})) : S c= S1 } implies ( ( conv (@ S) meets Int Aff implies card X = 2 ) & ( conv (@ S) misses Int Aff implies card X = 1 ) ) )
assume A8:
X = { S1 where S1 is Simplex of n, BCS (0,(Complex_of {Aff})) : S c= S1 }
;
( ( conv (@ S) meets Int Aff implies card X = 2 ) & ( conv (@ S) misses Int Aff implies card X = 1 ) )
A9:
X c= {Aff}
A12:
S in bool Aff
by A6, A7, PRE_TOPC:def 2;
A1 is
Simplex of
n,
Complex_of {Aff}
by A2, SIMPLEX0:48;
then
Aff in X
by A7, A8, A12;
then A13:
X = {Aff}
by A9, ZFMISC_1:33;
(
n + (- 1) >= - 1 &
n - 1
<= degree (Complex_of {Aff}) )
by A3, XREAL_1:31, XREAL_1:146;
then card S =
n1 + 1
by A7, SIMPLEX0:def 18
.=
(n - 1) + 1
by XXREAL_3:def 2
;
then
S <> Aff
by A1;
then
S c< Aff
by A12;
hence
( (
conv (@ S) meets Int Aff implies
card X = 2 ) & (
conv (@ S) misses Int Aff implies
card X = 1 ) )
by A13, CARD_1:30, RLAFFIN2:7;
verum
end;
A14:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A15:
S1[
k]
;
S1[k + 1]
A16:
(
degree (BCS (k,(Complex_of {Aff}))) = n &
BCS (
(k + 1),
(Complex_of {Aff}))
= BCS (BCS (k,(Complex_of {Aff}))) )
by A3, A4, Th20, Th32;
let S be
Simplex of
n - 1,
BCS (
(k + 1),
(Complex_of {Aff}));
for X being set st X = { S1 where S1 is Simplex of n, BCS ((k + 1),(Complex_of {Aff})) : S c= S1 } holds
( ( conv (@ S) meets Int Aff implies card X = 2 ) & ( conv (@ S) misses Int Aff implies card X = 1 ) )let X be
set ;
( X = { S1 where S1 is Simplex of n, BCS ((k + 1),(Complex_of {Aff})) : S c= S1 } implies ( ( conv (@ S) meets Int Aff implies card X = 2 ) & ( conv (@ S) misses Int Aff implies card X = 1 ) ) )
assume A17:
X = { S1 where S1 is Simplex of n, BCS ((k + 1),(Complex_of {Aff})) : S c= S1 }
;
( ( conv (@ S) meets Int Aff implies card X = 2 ) & ( conv (@ S) misses Int Aff implies card X = 1 ) )
thus
( (
conv (@ S) meets Int Aff implies
card X = 2 ) & (
conv (@ S) misses Int Aff implies
card X = 1 ) )
by A1, A15, A16, A17, Th44;
verum
end;
for k being Nat holds S1[k]
from NAT_1:sch 2(A5, A14);
hence
( not X = { S1 where S1 is Simplex of n, BCS (k,(Complex_of {Aff})) : S c= S1 } or ( ( conv (@ S) meets Int Aff implies card X = 2 ) & ( conv (@ S) misses Int Aff implies card X = 1 ) ) )
; verum