:: by Karol P\kak

::

:: Received December 21, 2010

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

reconsider jj = 1 as positive Real ;

definition

let M be non empty MetrSpace;

assume A1: TopSpaceMetr M is compact ;

let F be Subset-Family of (TopSpaceMetr M);

assume that

A2: F is open and

A3: F is Cover of (TopSpaceMetr M) ;

ex b_{1} being positive Real st

for p being Point of M ex A being Subset of (TopSpaceMetr M) st

( A in F & Ball (p,b_{1}) c= A )

end;
assume A1: TopSpaceMetr M is compact ;

let F be Subset-Family of (TopSpaceMetr M);

assume that

A2: F is open and

A3: F is Cover of (TopSpaceMetr M) ;

mode Lebesgue_number of F -> positive Real means :Def1: :: SIMPLEX2:def 1

for p being Point of M ex A being Subset of (TopSpaceMetr M) st

( A in F & Ball (p,it) c= A );

existence for p being Point of M ex A being Subset of (TopSpaceMetr M) st

( A in F & Ball (p,it) c= A );

ex b

for p being Point of M ex A being Subset of (TopSpaceMetr M) st

( A in F & Ball (p,b

proof end;

:: deftheorem Def1 defines Lebesgue_number SIMPLEX2:def 1 :

for M being non empty MetrSpace st TopSpaceMetr M is compact holds

for F being Subset-Family of (TopSpaceMetr M) st F is open & F is Cover of (TopSpaceMetr M) holds

for b_{3} being positive Real holds

( b_{3} is Lebesgue_number of F iff for p being Point of M ex A being Subset of (TopSpaceMetr M) st

( A in F & Ball (p,b_{3}) c= A ) );

for M being non empty MetrSpace st TopSpaceMetr M is compact holds

for F being Subset-Family of (TopSpaceMetr M) st F is open & F is Cover of (TopSpaceMetr M) holds

for b

( b

( A in F & Ball (p,b

theorem :: SIMPLEX2:1

for M being non empty MetrSpace

for F, G being open Subset-Family of (TopSpaceMetr M)

for L being Lebesgue_number of F st TopSpaceMetr M is compact & F is Cover of (TopSpaceMetr M) & F c= G holds

L is Lebesgue_number of G

for F, G being open Subset-Family of (TopSpaceMetr M)

for L being Lebesgue_number of F st TopSpaceMetr M is compact & F is Cover of (TopSpaceMetr M) & F c= G holds

L is Lebesgue_number of G

proof end;

theorem :: SIMPLEX2:2

for M being non empty MetrSpace

for F, G being open Subset-Family of (TopSpaceMetr M)

for L being Lebesgue_number of F st TopSpaceMetr M is compact & F is Cover of (TopSpaceMetr M) & F is_finer_than G holds

L is Lebesgue_number of G

for F, G being open Subset-Family of (TopSpaceMetr M)

for L being Lebesgue_number of F st TopSpaceMetr M is compact & F is Cover of (TopSpaceMetr M) & F is_finer_than G holds

L is Lebesgue_number of G

proof end;

theorem :: SIMPLEX2:3

for M being non empty MetrSpace

for F being open Subset-Family of (TopSpaceMetr M)

for L being Lebesgue_number of F

for L1 being positive Real st TopSpaceMetr M is compact & F is Cover of (TopSpaceMetr M) & L1 <= L holds

L1 is Lebesgue_number of F

for F being open Subset-Family of (TopSpaceMetr M)

for L being Lebesgue_number of F

for L1 being positive Real st TopSpaceMetr M is compact & F is Cover of (TopSpaceMetr M) & L1 <= L holds

L1 is Lebesgue_number of F

proof end;

registration

let M be non empty Reflexive MetrStruct ;

coherence

for b_{1} being Subset of M st b_{1} is finite holds

b_{1} is bounded

end;
coherence

for b

b

proof end;

theorem :: SIMPLEX2:4

for M being non empty Reflexive MetrStruct

for S being non empty finite Subset of M ex p, q being Point of M st

( p in S & q in S & dist (p,q) = diameter S )

for S being non empty finite Subset of M ex p, q being Point of M st

( p in S & q in S & dist (p,q) = diameter S )

proof end;

:: deftheorem Def2 defines bounded SIMPLEX2:def 2 :

for M being non empty Reflexive MetrStruct

for K being SimplicialComplexStr holds

( K is M bounded iff ex r being Real st

for A being Subset of M st A in the topology of K holds

( A is bounded & diameter A <= r ) );

for M being non empty Reflexive MetrStruct

for K being SimplicialComplexStr holds

( K is M bounded iff ex r being Real st

for A being Subset of M st A in the topology of K holds

( A is bounded & diameter A <= r ) );

theorem Th5: :: SIMPLEX2:5

for M being non empty Reflexive MetrStruct

for A being Subset of M

for K being non void SimplicialComplexStr st K is M bounded & A is Simplex of K holds

A is bounded

for A being Subset of M

for K being non void SimplicialComplexStr st K is M bounded & A is Simplex of K holds

A is bounded

proof end;

registration

let M be non empty Reflexive MetrStruct ;

let X be set ;

existence

ex b_{1} being SimplicialComplex of X st

( b_{1} is M bounded & not b_{1} is void )

end;
let X be set ;

existence

ex b

( b

proof end;

registration

let M be non empty Reflexive MetrStruct ;

existence

ex b_{1} being SimplicialComplexStr st

( b_{1} is M bounded & not b_{1} is void & b_{1} is subset-closed & b_{1} is finite-membered )

end;
existence

ex b

( b

proof end;

registration

let M be non empty Reflexive MetrStruct ;

let X be set ;

let K be M bounded SimplicialComplexStr of X;

coherence

for b_{1} being SubSimplicialComplex of K holds b_{1} is M bounded

end;
let X be set ;

let K be M bounded SimplicialComplexStr of X;

coherence

for b

proof end;

registration

let M be non empty Reflexive MetrStruct ;

let X be set ;

let K be subset-closed M bounded SimplicialComplexStr of X;

let i be dim-like number ;

coherence

Skeleton_of (K,i) is M bounded ;

end;
let X be set ;

let K be subset-closed M bounded SimplicialComplexStr of X;

let i be dim-like number ;

coherence

Skeleton_of (K,i) is M bounded ;

theorem Th6: :: SIMPLEX2:6

for M being non empty Reflexive MetrStruct

for K being SimplicialComplexStr st K is finite-vertices holds

K is M bounded

for K being SimplicialComplexStr st K is finite-vertices holds

K is M bounded

proof end;

definition

let M be non empty Reflexive MetrStruct ;

let K be SimplicialComplexStr;

assume A1: K is M bounded ;

( ( the topology of K meets bool ([#] M) implies ex b_{1} being Real st

( ( for A being Subset of M st A in the topology of K holds

diameter A <= b_{1} ) & ( for r being Real st ( for A being Subset of M st A in the topology of K holds

diameter A <= r ) holds

r >= b_{1} ) ) ) & ( not the topology of K meets bool ([#] M) implies ex b_{1} being Real st b_{1} = 0 ) )

for b_{1}, b_{2} being Real holds

( ( the topology of K meets bool ([#] M) & ( for A being Subset of M st A in the topology of K holds

diameter A <= b_{1} ) & ( for r being Real st ( for A being Subset of M st A in the topology of K holds

diameter A <= r ) holds

r >= b_{1} ) & ( for A being Subset of M st A in the topology of K holds

diameter A <= b_{2} ) & ( for r being Real st ( for A being Subset of M st A in the topology of K holds

diameter A <= r ) holds

r >= b_{2} ) implies b_{1} = b_{2} ) & ( not the topology of K meets bool ([#] M) & b_{1} = 0 & b_{2} = 0 implies b_{1} = b_{2} ) )

for b_{1} being Real holds verum
;

end;
let K be SimplicialComplexStr;

assume A1: K is M bounded ;

func diameter (M,K) -> Real means :Def3: :: SIMPLEX2:def 3

( ( for A being Subset of M st A in the topology of K holds

diameter A <= it ) & ( for r being Real st ( for A being Subset of M st A in the topology of K holds

diameter A <= r ) holds

r >= it ) ) if the topology of K meets bool ([#] M)

otherwise it = 0 ;

existence ( ( for A being Subset of M st A in the topology of K holds

diameter A <= it ) & ( for r being Real st ( for A being Subset of M st A in the topology of K holds

diameter A <= r ) holds

r >= it ) ) if the topology of K meets bool ([#] M)

otherwise it = 0 ;

( ( the topology of K meets bool ([#] M) implies ex b

( ( for A being Subset of M st A in the topology of K holds

diameter A <= b

diameter A <= r ) holds

r >= b

proof end;

uniqueness for b

( ( the topology of K meets bool ([#] M) & ( for A being Subset of M st A in the topology of K holds

diameter A <= b

diameter A <= r ) holds

r >= b

diameter A <= b

diameter A <= r ) holds

r >= b

proof end;

consistency for b

:: deftheorem Def3 defines diameter SIMPLEX2:def 3 :

for M being non empty Reflexive MetrStruct

for K being SimplicialComplexStr st K is M bounded holds

for b_{3} being Real holds

( ( the topology of K meets bool ([#] M) implies ( b_{3} = diameter (M,K) iff ( ( for A being Subset of M st A in the topology of K holds

diameter A <= b_{3} ) & ( for r being Real st ( for A being Subset of M st A in the topology of K holds

diameter A <= r ) holds

r >= b_{3} ) ) ) ) & ( not the topology of K meets bool ([#] M) implies ( b_{3} = diameter (M,K) iff b_{3} = 0 ) ) );

for M being non empty Reflexive MetrStruct

for K being SimplicialComplexStr st K is M bounded holds

for b

( ( the topology of K meets bool ([#] M) implies ( b

diameter A <= b

diameter A <= r ) holds

r >= b

theorem Th7: :: SIMPLEX2:7

for M being non empty Reflexive MetrStruct

for K being SimplicialComplexStr st K is M bounded holds

0 <= diameter (M,K)

for K being SimplicialComplexStr st K is M bounded holds

0 <= diameter (M,K)

proof end;

theorem :: SIMPLEX2:8

for X being set

for M being non empty Reflexive MetrStruct

for K being b_{2} bounded SimplicialComplexStr of X

for KX being SubSimplicialComplex of K holds diameter (M,KX) <= diameter (M,K)

for M being non empty Reflexive MetrStruct

for K being b

for KX being SubSimplicialComplex of K holds diameter (M,KX) <= diameter (M,K)

proof end;

theorem :: SIMPLEX2:9

for X being set

for M being non empty Reflexive MetrStruct

for K being subset-closed b_{2} bounded SimplicialComplexStr of X

for i being dim-like number holds diameter (M,(Skeleton_of (K,i))) <= diameter (M,K)

for M being non empty Reflexive MetrStruct

for K being subset-closed b

for i being dim-like number holds diameter (M,(Skeleton_of (K,i))) <= diameter (M,K)

proof end;

definition

let M be non empty Reflexive MetrStruct ;

let K be non void subset-closed M bounded SimplicialComplexStr;

for b_{1} being Real holds

( b_{1} = diameter (M,K) iff ( ( for A being Subset of M st A is Simplex of K holds

diameter A <= b_{1} ) & ( for r being Real st ( for A being Subset of M st A is Simplex of K holds

diameter A <= r ) holds

r >= b_{1} ) ) )

end;
let K be non void subset-closed M bounded SimplicialComplexStr;

redefine func diameter (M,K) means :Def4: :: SIMPLEX2:def 4

( ( for A being Subset of M st A is Simplex of K holds

diameter A <= it ) & ( for r being Real st ( for A being Subset of M st A is Simplex of K holds

diameter A <= r ) holds

r >= it ) );

compatibility ( ( for A being Subset of M st A is Simplex of K holds

diameter A <= it ) & ( for r being Real st ( for A being Subset of M st A is Simplex of K holds

diameter A <= r ) holds

r >= it ) );

for b

( b

diameter A <= b

diameter A <= r ) holds

r >= b

proof end;

:: deftheorem Def4 defines diameter SIMPLEX2:def 4 :

for M being non empty Reflexive MetrStruct

for K being non void subset-closed b_{1} bounded SimplicialComplexStr

for b_{3} being Real holds

( b_{3} = diameter (M,K) iff ( ( for A being Subset of M st A is Simplex of K holds

diameter A <= b_{3} ) & ( for r being Real st ( for A being Subset of M st A is Simplex of K holds

diameter A <= r ) holds

r >= b_{3} ) ) );

for M being non empty Reflexive MetrStruct

for K being non void subset-closed b

for b

( b

diameter A <= b

diameter A <= r ) holds

r >= b

theorem :: SIMPLEX2:10

for M being non empty Reflexive MetrStruct

for S being finite Subset of M holds diameter (M,(Complex_of {S})) = diameter S

for S being finite Subset of M holds diameter (M,(Complex_of {S})) = diameter S

proof end;

definition

let n be Nat;

let K be SimplicialComplexStr of (TOP-REAL n);

coherence

diameter ((Euclid n),K) is Real ;

end;
let K be SimplicialComplexStr of (TOP-REAL n);

coherence

diameter ((Euclid n),K) is Real ;

:: deftheorem defines bounded SIMPLEX2:def 5 :

for n being Nat

for K being SimplicialComplexStr of (TOP-REAL n) holds

( K is bounded iff K is Euclid n bounded );

for n being Nat

for K being SimplicialComplexStr of (TOP-REAL n) holds

( K is bounded iff K is Euclid n bounded );

:: deftheorem defines diameter SIMPLEX2:def 6 :

for n being Nat

for K being SimplicialComplexStr of (TOP-REAL n) holds diameter K = diameter ((Euclid n),K);

for n being Nat

for K being SimplicialComplexStr of (TOP-REAL n) holds diameter K = diameter ((Euclid n),K);

registration

let n be Nat;

coherence

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

b_{1} is Euclid n bounded
;

ex b_{1} being SimplicialComplex of (TOP-REAL n) st

( b_{1} is bounded & b_{1} is affinely-independent & b_{1} is simplex-join-closed & not b_{1} is void & b_{1} is finite-degree & b_{1} is total )

for b_{1} being SimplicialComplexStr of (TOP-REAL n) st b_{1} is finite-vertices holds

b_{1} is bounded
by Th6;

end;
coherence

for b

b

cluster non void subset-closed finite-membered finite-degree total affinely-independent simplex-join-closed bounded for SimplicialComplexStr of the carrier of (TOP-REAL n);

existence ex b

( b

proof end;

coherence for b

b

Lm1: for n being Nat holds [#] (TOP-REAL n) = [#] (Euclid n)

proof end;

Lm2: for x being set holds {x} is c=-linear

proof end;

theorem Th11: :: SIMPLEX2:11

for V being RealLinearSpace

for Kv being non void SimplicialComplex of V

for S being Simplex of (BCS Kv)

for F being c=-linear finite finite-membered Subset-Family of V st S = (center_of_mass V) .: F holds

for a1, a2 being VECTOR of V st a1 in S & a2 in S holds

ex b1, b2 being VECTOR of V ex r being Real st

( b1 in Vertices (BCS (Complex_of {(union F)})) & b2 in Vertices (BCS (Complex_of {(union F)})) & a1 - a2 = r * (b1 - b2) & 0 <= r & r <= ((card (union F)) - 1) / (card (union F)) )

for Kv being non void SimplicialComplex of V

for S being Simplex of (BCS Kv)

for F being c=-linear finite finite-membered Subset-Family of V st S = (center_of_mass V) .: F holds

for a1, a2 being VECTOR of V st a1 in S & a2 in S holds

ex b1, b2 being VECTOR of V ex r being Real st

( b1 in Vertices (BCS (Complex_of {(union F)})) & b2 in Vertices (BCS (Complex_of {(union F)})) & a1 - a2 = r * (b1 - b2) & 0 <= r & r <= ((card (union F)) - 1) / (card (union F)) )

proof end;

theorem Th12: :: SIMPLEX2:12

for n being Nat

for X being set

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

for E being Enumeration of A st not (dom E) \ X is empty holds

conv (E .: X) = meet { (conv (A \ {(E . k)})) where k is Element of NAT : k in (dom E) \ X }

for X being set

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

for E being Enumeration of A st not (dom E) \ X is empty holds

conv (E .: X) = meet { (conv (A \ {(E . k)})) where k is Element of NAT : k in (dom E) \ X }

proof end;

theorem Th13: :: SIMPLEX2:13

for n being Nat

for A being Subset of (TOP-REAL n)

for a being bounded Subset of (Euclid n) st a = A holds

for p being Point of (Euclid n) st p in conv A holds

conv A c= cl_Ball (p,(diameter a))

for A being Subset of (TOP-REAL n)

for a being bounded Subset of (Euclid n) st a = A holds

for p being Point of (Euclid n) st p in conv A holds

conv A c= cl_Ball (p,(diameter a))

proof end;

theorem Th15: :: SIMPLEX2:15

for n being Nat

for A being Subset of (TOP-REAL n)

for a, ca being bounded Subset of (Euclid n) st ca = conv A & a = A holds

diameter a = diameter ca

for A being Subset of (TOP-REAL n)

for a, ca being bounded Subset of (Euclid n) st ca = conv A & a = A holds

diameter a = diameter ca

proof end;

registration

let n be Nat;

let K be bounded SimplicialComplexStr of (TOP-REAL n);

coherence

for b_{1} being SubdivisionStr of K holds b_{1} is bounded

end;
let K be bounded SimplicialComplexStr of (TOP-REAL n);

coherence

for b

proof end;

theorem Th16: :: SIMPLEX2:16

for n being Nat

for K being non void finite-degree bounded SimplicialComplex of (TOP-REAL n) st |.K.| c= [#] K holds

diameter (BCS K) <= ((degree K) / ((degree K) + 1)) * (diameter K)

for K being non void finite-degree bounded SimplicialComplex of (TOP-REAL n) st |.K.| c= [#] K holds

diameter (BCS K) <= ((degree K) / ((degree K) + 1)) * (diameter K)

proof end;

theorem Th17: :: SIMPLEX2:17

for n, k being Nat

for K being non void finite-degree bounded SimplicialComplex of (TOP-REAL n) st |.K.| c= [#] K holds

diameter (BCS (k,K)) <= (((degree K) / ((degree K) + 1)) |^ k) * (diameter K)

for K being non void finite-degree bounded SimplicialComplex of (TOP-REAL n) st |.K.| c= [#] K holds

diameter (BCS (k,K)) <= (((degree K) / ((degree K) + 1)) |^ k) * (diameter K)

proof end;

theorem Th18: :: SIMPLEX2:18

for n being Nat

for K being non void finite-degree bounded SimplicialComplex of (TOP-REAL n) st |.K.| c= [#] K holds

for r being Real st r > 0 holds

ex k being Nat st diameter (BCS (k,K)) < r

for K being non void finite-degree bounded SimplicialComplex of (TOP-REAL n) st |.K.| c= [#] K holds

for r being Real st r > 0 holds

ex k being Nat st diameter (BCS (k,K)) < r

proof end;

theorem Th19: :: SIMPLEX2:19

for i, j being Element of NAT ex f being Function of [:(TOP-REAL i),(TOP-REAL j):],(TOP-REAL (i + j)) st

( f is being_homeomorphism & ( for fi being Element of (TOP-REAL i)

for fj being Element of (TOP-REAL j) holds f . (fi,fj) = fi ^ fj ) )

( f is being_homeomorphism & ( for fi being Element of (TOP-REAL i)

for fj being Element of (TOP-REAL j) holds f . (fi,fj) = fi ^ fj ) )

proof end;

Lm3: for n being Nat holds [#] (TOP-REAL n) = [#] (TopSpaceMetr (Euclid n))

proof end;

theorem Th20: :: SIMPLEX2:20

for i, j being Element of NAT

for f being Function of [:(TOP-REAL i),(TOP-REAL j):],(TOP-REAL (i + j)) st ( for fi being Element of (TOP-REAL i)

for fj being Element of (TOP-REAL j) holds f . (fi,fj) = fi ^ fj ) holds

for r being Real

for fi being Point of (Euclid i)

for fj being Point of (Euclid j)

for fij being Point of (Euclid (i + j)) st fij = fi ^ fj holds

f .: [:(OpenHypercube (fi,r)),(OpenHypercube (fj,r)):] = OpenHypercube (fij,r)

for f being Function of [:(TOP-REAL i),(TOP-REAL j):],(TOP-REAL (i + j)) st ( for fi being Element of (TOP-REAL i)

for fj being Element of (TOP-REAL j) holds f . (fi,fj) = fi ^ fj ) holds

for r being Real

for fi being Point of (Euclid i)

for fj being Point of (Euclid j)

for fij being Point of (Euclid (i + j)) st fij = fi ^ fj holds

f .: [:(OpenHypercube (fi,r)),(OpenHypercube (fj,r)):] = OpenHypercube (fij,r)

proof end;

theorem Th21: :: SIMPLEX2:21

for n being Nat

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

( A is bounded iff ex p being Point of (Euclid n) ex r being Real st A c= OpenHypercube (p,r) )

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

( A is bounded iff ex p being Point of (Euclid n) ex r being Real st A c= OpenHypercube (p,r) )

proof end;

Lm4: for A being Subset of (TOP-REAL 1) st A is closed & A is bounded holds

A is compact

proof end;

Lm5: for n being Nat

for A being Subset of (TOP-REAL n) st A is closed & A is bounded holds

A is compact

proof end;

registration

let n be Nat;

coherence

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

b_{1} is compact
by Lm5;

end;
coherence

for b

b

registration

let n be Nat;

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

coherence

conv A is compact

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

coherence

conv A is compact

proof end;

theorem Th22: :: SIMPLEX2:22

for n being Nat

for A being non empty affinely-independent Subset of (TOP-REAL n)

for E being Enumeration of A

for F being FinSequence of bool the carrier of ((TOP-REAL n) | (conv A)) st len F = card A & rng F is closed & ( for S being Subset of (dom F) holds conv (E .: S) c= union (F .: S) ) holds

not meet (rng F) is empty

for A being non empty affinely-independent Subset of (TOP-REAL n)

for E being Enumeration of A

for F being FinSequence of bool the carrier of ((TOP-REAL n) | (conv A)) st len F = card A & rng F is closed & ( for S being Subset of (dom F) holds conv (E .: S) c= union (F .: S) ) holds

not meet (rng F) is empty

proof end;

theorem Th23: :: SIMPLEX2:23

for n being Nat

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

for f being continuous Function of ((TOP-REAL n) | (conv A)),((TOP-REAL n) | (conv A)) ex p being Point of (TOP-REAL n) st

( p in dom f & f . p = p )

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

for f being continuous Function of ((TOP-REAL n) | (conv A)),((TOP-REAL n) | (conv A)) ex p being Point of (TOP-REAL n) st

( p in dom f & f . p = p )

proof end;

theorem :: SIMPLEX2:24

for n being Nat

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

for f being continuous Function of ((TOP-REAL n) | (conv A)),((TOP-REAL n) | (conv A)) holds f is with_fixpoint

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

for f being continuous Function of ((TOP-REAL n) | (conv A)),((TOP-REAL n) | (conv A)) holds f is with_fixpoint

proof end;

theorem Th25: :: SIMPLEX2:25

for n being Nat

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

ind (conv A) = n

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

ind (conv A) = n

proof end;