:: CONVEX2 semantic presentation
begin
theorem
:: CONVEX2:1
for
V
being ( ( non
empty
) ( non
empty
)
RLSStruct
)
for
M
,
N
being ( (
convex
) (
convex
)
Subset
of ) holds
M
: ( (
convex
) (
convex
)
Subset
of )
/\
N
: ( (
convex
) (
convex
)
Subset
of ) : ( ( ) (
convex
)
Element
of
K48
( the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) is
convex
;
theorem
:: CONVEX2:2
for
V
being ( ( non
empty
RealUnitarySpace-like
) ( non
empty
RealUnitarySpace-like
)
UNITSTR
)
for
M
being ( ( ) ( )
Subset
of )
for
F
being ( ( ) (
Relation-like
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
RealUnitarySpace-like
) ( non
empty
RealUnitarySpace-like
)
UNITSTR
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of the
carrier
of
V
: ( ( non
empty
RealUnitarySpace-like
) ( non
empty
RealUnitarySpace-like
)
UNITSTR
) : ( ( ) ( non
empty
)
set
) )
for
B
being ( ( ) (
Relation-like
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
V123
()
V124
()
V125
() )
FinSequence
of
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) st
M
: ( ( ) ( )
Subset
of )
=
{
u
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) where
u
is ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) : for
i
being ( ( ) (
V8
()
V12
()
V24
()
V25
()
V30
()
V31
()
ext-real
non
negative
V133
()
V134
()
V135
()
V136
()
V137
()
V138
() )
Element
of
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) ) ) st
i
: ( ( ) (
V8
()
V12
()
V24
()
V25
()
V30
()
V31
()
ext-real
non
negative
V133
()
V134
()
V135
()
V136
()
V137
()
V138
() )
Element
of
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) ) )
in
(
dom
F
: ( ( ) (
Relation-like
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
RealUnitarySpace-like
) ( non
empty
RealUnitarySpace-like
)
UNITSTR
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of the
carrier
of
b
1
: ( ( non
empty
RealUnitarySpace-like
) ( non
empty
RealUnitarySpace-like
)
UNITSTR
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
() )
Element
of
K48
(
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) )
/\
(
dom
B
: ( ( ) (
Relation-like
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
V123
()
V124
()
V125
() )
FinSequence
of
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) )
)
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
() )
Element
of
K48
(
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) : ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
() )
Element
of
K48
(
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) holds
ex
v
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) st
(
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
=
F
: ( ( ) (
Relation-like
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
RealUnitarySpace-like
) ( non
empty
RealUnitarySpace-like
)
UNITSTR
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of the
carrier
of
b
1
: ( ( non
empty
RealUnitarySpace-like
) ( non
empty
RealUnitarySpace-like
)
UNITSTR
) : ( ( ) ( non
empty
)
set
) )
.
i
: ( ( ) (
V8
()
V12
()
V24
()
V25
()
V30
()
V31
()
ext-real
non
negative
V133
()
V134
()
V135
()
V136
()
V137
()
V138
() )
Element
of
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) &
u
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
.|.
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
V24
()
V25
()
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) )
<=
B
: ( ( ) (
Relation-like
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
V123
()
V124
()
V125
() )
FinSequence
of
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) )
.
i
: ( ( ) (
V8
()
V12
()
V24
()
V25
()
V30
()
V31
()
ext-real
non
negative
V133
()
V134
()
V135
()
V136
()
V137
()
V138
() )
Element
of
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V24
()
V25
()
ext-real
)
set
) )
}
holds
M
: ( ( ) ( )
Subset
of ) is
convex
;
theorem
:: CONVEX2:3
for
V
being ( ( non
empty
RealUnitarySpace-like
) ( non
empty
RealUnitarySpace-like
)
UNITSTR
)
for
M
being ( ( ) ( )
Subset
of )
for
F
being ( ( ) (
Relation-like
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
RealUnitarySpace-like
) ( non
empty
RealUnitarySpace-like
)
UNITSTR
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of the
carrier
of
V
: ( ( non
empty
RealUnitarySpace-like
) ( non
empty
RealUnitarySpace-like
)
UNITSTR
) : ( ( ) ( non
empty
)
set
) )
for
B
being ( ( ) (
Relation-like
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
V123
()
V124
()
V125
() )
FinSequence
of
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) st
M
: ( ( ) ( )
Subset
of )
=
{
u
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) where
u
is ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) : for
i
being ( ( ) (
V8
()
V12
()
V24
()
V25
()
V30
()
V31
()
ext-real
non
negative
V133
()
V134
()
V135
()
V136
()
V137
()
V138
() )
Element
of
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) ) ) st
i
: ( ( ) (
V8
()
V12
()
V24
()
V25
()
V30
()
V31
()
ext-real
non
negative
V133
()
V134
()
V135
()
V136
()
V137
()
V138
() )
Element
of
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) ) )
in
(
dom
F
: ( ( ) (
Relation-like
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
RealUnitarySpace-like
) ( non
empty
RealUnitarySpace-like
)
UNITSTR
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of the
carrier
of
b
1
: ( ( non
empty
RealUnitarySpace-like
) ( non
empty
RealUnitarySpace-like
)
UNITSTR
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
() )
Element
of
K48
(
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) )
/\
(
dom
B
: ( ( ) (
Relation-like
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
V123
()
V124
()
V125
() )
FinSequence
of
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) )
)
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
() )
Element
of
K48
(
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) : ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
() )
Element
of
K48
(
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) holds
ex
v
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) st
(
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
=
F
: ( ( ) (
Relation-like
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
RealUnitarySpace-like
) ( non
empty
RealUnitarySpace-like
)
UNITSTR
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of the
carrier
of
b
1
: ( ( non
empty
RealUnitarySpace-like
) ( non
empty
RealUnitarySpace-like
)
UNITSTR
) : ( ( ) ( non
empty
)
set
) )
.
i
: ( ( ) (
V8
()
V12
()
V24
()
V25
()
V30
()
V31
()
ext-real
non
negative
V133
()
V134
()
V135
()
V136
()
V137
()
V138
() )
Element
of
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) &
u
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
.|.
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
V24
()
V25
()
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) )
<
B
: ( ( ) (
Relation-like
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
V123
()
V124
()
V125
() )
FinSequence
of
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) )
.
i
: ( ( ) (
V8
()
V12
()
V24
()
V25
()
V30
()
V31
()
ext-real
non
negative
V133
()
V134
()
V135
()
V136
()
V137
()
V138
() )
Element
of
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V24
()
V25
()
ext-real
)
set
) )
}
holds
M
: ( ( ) ( )
Subset
of ) is
convex
;
theorem
:: CONVEX2:4
for
V
being ( ( non
empty
RealUnitarySpace-like
) ( non
empty
RealUnitarySpace-like
)
UNITSTR
)
for
M
being ( ( ) ( )
Subset
of )
for
F
being ( ( ) (
Relation-like
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
RealUnitarySpace-like
) ( non
empty
RealUnitarySpace-like
)
UNITSTR
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of the
carrier
of
V
: ( ( non
empty
RealUnitarySpace-like
) ( non
empty
RealUnitarySpace-like
)
UNITSTR
) : ( ( ) ( non
empty
)
set
) )
for
B
being ( ( ) (
Relation-like
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
V123
()
V124
()
V125
() )
FinSequence
of
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) st
M
: ( ( ) ( )
Subset
of )
=
{
u
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) where
u
is ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) : for
i
being ( ( ) (
V8
()
V12
()
V24
()
V25
()
V30
()
V31
()
ext-real
non
negative
V133
()
V134
()
V135
()
V136
()
V137
()
V138
() )
Element
of
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) ) ) st
i
: ( ( ) (
V8
()
V12
()
V24
()
V25
()
V30
()
V31
()
ext-real
non
negative
V133
()
V134
()
V135
()
V136
()
V137
()
V138
() )
Element
of
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) ) )
in
(
dom
F
: ( ( ) (
Relation-like
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
RealUnitarySpace-like
) ( non
empty
RealUnitarySpace-like
)
UNITSTR
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of the
carrier
of
b
1
: ( ( non
empty
RealUnitarySpace-like
) ( non
empty
RealUnitarySpace-like
)
UNITSTR
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
() )
Element
of
K48
(
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) )
/\
(
dom
B
: ( ( ) (
Relation-like
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
V123
()
V124
()
V125
() )
FinSequence
of
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) )
)
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
() )
Element
of
K48
(
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) : ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
() )
Element
of
K48
(
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) holds
ex
v
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) st
(
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
=
F
: ( ( ) (
Relation-like
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
RealUnitarySpace-like
) ( non
empty
RealUnitarySpace-like
)
UNITSTR
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of the
carrier
of
b
1
: ( ( non
empty
RealUnitarySpace-like
) ( non
empty
RealUnitarySpace-like
)
UNITSTR
) : ( ( ) ( non
empty
)
set
) )
.
i
: ( ( ) (
V8
()
V12
()
V24
()
V25
()
V30
()
V31
()
ext-real
non
negative
V133
()
V134
()
V135
()
V136
()
V137
()
V138
() )
Element
of
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) &
u
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
.|.
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
V24
()
V25
()
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) )
>=
B
: ( ( ) (
Relation-like
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
V123
()
V124
()
V125
() )
FinSequence
of
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) )
.
i
: ( ( ) (
V8
()
V12
()
V24
()
V25
()
V30
()
V31
()
ext-real
non
negative
V133
()
V134
()
V135
()
V136
()
V137
()
V138
() )
Element
of
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V24
()
V25
()
ext-real
)
set
) )
}
holds
M
: ( ( ) ( )
Subset
of ) is
convex
;
theorem
:: CONVEX2:5
for
V
being ( ( non
empty
RealUnitarySpace-like
) ( non
empty
RealUnitarySpace-like
)
UNITSTR
)
for
M
being ( ( ) ( )
Subset
of )
for
F
being ( ( ) (
Relation-like
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
RealUnitarySpace-like
) ( non
empty
RealUnitarySpace-like
)
UNITSTR
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of the
carrier
of
V
: ( ( non
empty
RealUnitarySpace-like
) ( non
empty
RealUnitarySpace-like
)
UNITSTR
) : ( ( ) ( non
empty
)
set
) )
for
B
being ( ( ) (
Relation-like
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
V123
()
V124
()
V125
() )
FinSequence
of
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) st
M
: ( ( ) ( )
Subset
of )
=
{
u
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) where
u
is ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) : for
i
being ( ( ) (
V8
()
V12
()
V24
()
V25
()
V30
()
V31
()
ext-real
non
negative
V133
()
V134
()
V135
()
V136
()
V137
()
V138
() )
Element
of
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) ) ) st
i
: ( ( ) (
V8
()
V12
()
V24
()
V25
()
V30
()
V31
()
ext-real
non
negative
V133
()
V134
()
V135
()
V136
()
V137
()
V138
() )
Element
of
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) ) )
in
(
dom
F
: ( ( ) (
Relation-like
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
RealUnitarySpace-like
) ( non
empty
RealUnitarySpace-like
)
UNITSTR
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of the
carrier
of
b
1
: ( ( non
empty
RealUnitarySpace-like
) ( non
empty
RealUnitarySpace-like
)
UNITSTR
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
() )
Element
of
K48
(
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) )
/\
(
dom
B
: ( ( ) (
Relation-like
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
V123
()
V124
()
V125
() )
FinSequence
of
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) )
)
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
() )
Element
of
K48
(
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) : ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
() )
Element
of
K48
(
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) holds
ex
v
being ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) st
(
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
=
F
: ( ( ) (
Relation-like
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) )
-defined
the
carrier
of
b
1
: ( ( non
empty
RealUnitarySpace-like
) ( non
empty
RealUnitarySpace-like
)
UNITSTR
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
)
FinSequence
of the
carrier
of
b
1
: ( ( non
empty
RealUnitarySpace-like
) ( non
empty
RealUnitarySpace-like
)
UNITSTR
) : ( ( ) ( non
empty
)
set
) )
.
i
: ( ( ) (
V8
()
V12
()
V24
()
V25
()
V30
()
V31
()
ext-real
non
negative
V133
()
V134
()
V135
()
V136
()
V137
()
V138
() )
Element
of
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) &
u
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) )
.|.
v
: ( ( ) ( )
VECTOR
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
V24
()
V25
()
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) )
>
B
: ( ( ) (
Relation-like
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
finite
FinSequence-like
FinSubsequence-like
V123
()
V124
()
V125
() )
FinSequence
of
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) )
.
i
: ( ( ) (
V8
()
V12
()
V24
()
V25
()
V30
()
V31
()
ext-real
non
negative
V133
()
V134
()
V135
()
V136
()
V137
()
V138
() )
Element
of
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V24
()
V25
()
ext-real
)
set
) )
}
holds
M
: ( ( ) ( )
Subset
of ) is
convex
;
theorem
:: CONVEX2:6
for
V
being ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
)
for
M
being ( ( ) ( )
Subset
of ) holds
( ( for
N
being ( ( ) ( )
Subset
of )
for
L
being ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
quasi_total
V123
()
V124
()
V125
() )
Linear_Combination
of
N
: ( ( ) ( )
Subset
of ) ) st
L
: ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
quasi_total
V123
()
V124
()
V125
() )
Linear_Combination
of
b
3
: ( ( ) ( )
Subset
of ) ) is
convex
&
N
: ( ( ) ( )
Subset
of )
c=
M
: ( ( ) ( )
Subset
of ) holds
Sum
L
: ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
quasi_total
V123
()
V124
()
V125
() )
Linear_Combination
of
b
3
: ( ( ) ( )
Subset
of ) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) )
in
M
: ( ( ) ( )
Subset
of ) ) iff
M
: ( ( ) ( )
Subset
of ) is
convex
) ;
definition
let
V
be ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) ;
let
M
be ( ( ) ( )
Subset
of ) ;
func
LinComb
M
->
( ( ) ( )
set
)
means
:: CONVEX2:def 1
for
L
being ( ( ) ( )
set
) holds
(
L
: ( ( ) ( )
set
)
in
it
: ( (
Function-like
quasi_total
) (
Relation-like
K49
(
V
: ( ( ) ( )
UNITSTR
) ,
V
: ( ( ) ( )
UNITSTR
) ) : ( ( ) (
Relation-like
)
set
)
-defined
V
: ( ( ) ( )
UNITSTR
)
-valued
Function-like
quasi_total
)
Element
of
K48
(
K49
(
K49
(
V
: ( ( ) ( )
UNITSTR
) ,
V
: ( ( ) ( )
UNITSTR
) ) : ( ( ) (
Relation-like
)
set
) ,
V
: ( ( ) ( )
UNITSTR
) ) : ( ( ) (
Relation-like
)
set
) ) : ( ( ) ( )
set
) ) iff
L
: ( ( ) ( )
set
) is ( ( ) (
Relation-like
the
carrier
of
V
: ( ( ) ( )
UNITSTR
) : ( ( ) ( )
set
)
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
quasi_total
V123
()
V124
()
V125
() )
Linear_Combination
of
M
: ( ( ) ( )
Element
of
V
: ( ( ) ( )
UNITSTR
) ) ) );
end;
registration
let
V
be ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) ;
cluster
Relation-like
the
carrier
of
V
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
quasi_total
V123
()
V124
()
V125
()
convex
for ( ( ) ( )
Linear_Combination
of
V
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RLSStruct
) ) ;
end;
definition
let
V
be ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) ;
mode
Convex_Combination of
V
is
( (
convex
) (
Relation-like
the
carrier
of
V
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
quasi_total
V123
()
V124
()
V125
()
convex
)
Linear_Combination
of
V
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RLSStruct
) ) ;
end;
registration
let
V
be ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) ;
let
M
be ( ( non
empty
) ( non
empty
)
Subset
of ) ;
cluster
Relation-like
the
carrier
of
V
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
quasi_total
V123
()
V124
()
V125
()
convex
for ( ( ) ( )
Linear_Combination
of
M
: ( ( non
empty
) ( non
empty
)
Element
of
K48
( the
carrier
of
V
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ) ;
end;
definition
let
V
be ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) ;
let
M
be ( ( non
empty
) ( non
empty
)
Subset
of ) ;
mode
Convex_Combination of
M
is
( (
convex
) (
Relation-like
the
carrier
of
V
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
quasi_total
V123
()
V124
()
V125
()
convex
)
Linear_Combination
of
M
: ( ( non
empty
) ( non
empty
)
Element
of
K48
( the
carrier
of
V
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ) ;
end;
theorem
:: CONVEX2:7
for
V
being ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
)
for
M
being ( ( ) ( )
Subset
of ) holds
Convex-Family
M
: ( ( ) ( )
Subset
of ) : ( ( ) ( non
empty
)
Element
of
K48
(
K48
( the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
<>
{}
: ( ( ) (
Relation-like
non-empty
empty-yielding
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) )
-defined
RAT
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V136
()
V139
() )
set
)
-valued
empty
Function-like
one-to-one
constant
functional
finite
FinSequence-like
FinSubsequence-like
FinSequence-membered
V123
()
V124
()
V125
()
V126
()
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
set
) ;
theorem
:: CONVEX2:8
for
V
being ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
)
for
L1
,
L2
being ( (
convex
) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
quasi_total
V123
()
V124
()
V125
()
convex
)
Convex_Combination
of
V
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) )
for
r
being ( ( ) (
V24
()
V25
()
ext-real
)
Real
) st
0
: ( ( ) (
Relation-like
non-empty
empty-yielding
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) )
-defined
RAT
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V136
()
V139
() )
set
)
-valued
V8
()
V12
()
empty
Function-like
one-to-one
constant
functional
V24
()
V25
()
V30
()
V31
()
finite
FinSequence-like
FinSubsequence-like
FinSequence-membered
ext-real
non
positive
non
negative
V123
()
V124
()
V125
()
V126
()
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) ) )
<
r
: ( ( ) (
V24
()
V25
()
ext-real
)
Real
) &
r
: ( ( ) (
V24
()
V25
()
ext-real
)
Real
)
<
1 : ( ( ) (
V8
()
V12
() non
empty
V24
()
V25
()
V30
()
V31
()
ext-real
positive
non
negative
V133
()
V134
()
V135
()
V136
()
V137
()
V138
() )
Element
of
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
r
: ( ( ) (
V24
()
V25
()
ext-real
)
Real
)
*
L1
: ( (
convex
) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
quasi_total
V123
()
V124
()
V125
()
convex
)
Convex_Combination
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) )
)
: ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
quasi_total
V123
()
V124
()
V125
() )
Linear_Combination
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) )
+
(
(
1 : ( ( ) (
V8
()
V12
() non
empty
V24
()
V25
()
V30
()
V31
()
ext-real
positive
non
negative
V133
()
V134
()
V135
()
V136
()
V137
()
V138
() )
Element
of
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) ) )
-
r
: ( ( ) (
V24
()
V25
()
ext-real
)
Real
)
)
: ( ( ) (
V24
()
V25
()
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) )
*
L2
: ( (
convex
) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
quasi_total
V123
()
V124
()
V125
()
convex
)
Convex_Combination
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) )
)
: ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
quasi_total
V123
()
V124
()
V125
() )
Linear_Combination
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) ) : ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
quasi_total
V123
()
V124
()
V125
() )
Linear_Combination
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) ) is ( (
convex
) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
quasi_total
V123
()
V124
()
V125
()
convex
)
Convex_Combination
of
V
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) ) ;
theorem
:: CONVEX2:9
for
V
being ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
)
for
M
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
L1
,
L2
being ( (
convex
) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
quasi_total
V123
()
V124
()
V125
()
convex
)
Convex_Combination
of
M
: ( ( non
empty
) ( non
empty
)
Subset
of ) )
for
r
being ( ( ) (
V24
()
V25
()
ext-real
)
Real
) st
0
: ( ( ) (
Relation-like
non-empty
empty-yielding
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) )
-defined
RAT
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V136
()
V139
() )
set
)
-valued
V8
()
V12
()
empty
Function-like
one-to-one
constant
functional
V24
()
V25
()
V30
()
V31
()
finite
FinSequence-like
FinSubsequence-like
FinSequence-membered
ext-real
non
positive
non
negative
V123
()
V124
()
V125
()
V126
()
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) ) )
<
r
: ( ( ) (
V24
()
V25
()
ext-real
)
Real
) &
r
: ( ( ) (
V24
()
V25
()
ext-real
)
Real
)
<
1 : ( ( ) (
V8
()
V12
() non
empty
V24
()
V25
()
V30
()
V31
()
ext-real
positive
non
negative
V133
()
V134
()
V135
()
V136
()
V137
()
V138
() )
Element
of
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
r
: ( ( ) (
V24
()
V25
()
ext-real
)
Real
)
*
L1
: ( (
convex
) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
quasi_total
V123
()
V124
()
V125
()
convex
)
Convex_Combination
of
b
2
: ( ( non
empty
) ( non
empty
)
Subset
of ) )
)
: ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
quasi_total
V123
()
V124
()
V125
() )
Linear_Combination
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) )
+
(
(
1 : ( ( ) (
V8
()
V12
() non
empty
V24
()
V25
()
V30
()
V31
()
ext-real
positive
non
negative
V133
()
V134
()
V135
()
V136
()
V137
()
V138
() )
Element
of
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) ) )
-
r
: ( ( ) (
V24
()
V25
()
ext-real
)
Real
)
)
: ( ( ) (
V24
()
V25
()
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) )
*
L2
: ( (
convex
) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
quasi_total
V123
()
V124
()
V125
()
convex
)
Convex_Combination
of
b
2
: ( ( non
empty
) ( non
empty
)
Subset
of ) )
)
: ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
quasi_total
V123
()
V124
()
V125
() )
Linear_Combination
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) ) : ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
quasi_total
V123
()
V124
()
V125
() )
Linear_Combination
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) ) is ( (
convex
) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
quasi_total
V123
()
V124
()
V125
()
convex
)
Convex_Combination
of
M
: ( ( non
empty
) ( non
empty
)
Subset
of ) ) ;
begin
theorem
:: CONVEX2:10
for
V
being ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
)
for
W1
,
W2
being ( ( ) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
Subspace
of
V
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) ) holds
Up
(
W1
: ( ( ) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
Subspace
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) )
+
W2
: ( ( ) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
Subspace
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) )
)
: ( (
strict
) ( non
empty
V73
()
V74
()
strict
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
Subspace
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) ) : ( ( non
empty
) ( non
empty
)
Element
of
K48
( the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
(
Up
W1
: ( ( ) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
Subspace
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) )
)
: ( ( non
empty
) ( non
empty
)
Element
of
K48
( the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
+
(
Up
W2
: ( ( ) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
Subspace
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) )
)
: ( ( non
empty
) ( non
empty
)
Element
of
K48
( the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
K48
( the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: CONVEX2:11
for
V
being ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
)
for
W1
,
W2
being ( ( ) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
Subspace
of
V
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) ) holds
Up
(
W1
: ( ( ) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
Subspace
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) )
/\
W2
: ( ( ) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
Subspace
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) )
)
: ( (
strict
) ( non
empty
V73
()
V74
()
strict
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
Subspace
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) ) : ( ( non
empty
) ( non
empty
)
Element
of
K48
( the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
(
Up
W1
: ( ( ) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
Subspace
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) )
)
: ( ( non
empty
) ( non
empty
)
Element
of
K48
( the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
/\
(
Up
W2
: ( ( ) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
Subspace
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) )
)
: ( ( non
empty
) ( non
empty
)
Element
of
K48
( the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
K48
( the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: CONVEX2:12
for
V
being ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
)
for
L1
,
L2
being ( (
convex
) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
quasi_total
V123
()
V124
()
V125
()
convex
)
Convex_Combination
of
V
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) )
for
a
,
b
being ( ( ) (
V24
()
V25
()
ext-real
)
Real
) st
a
: ( ( ) (
V24
()
V25
()
ext-real
)
Real
)
*
b
: ( ( ) (
V24
()
V25
()
ext-real
)
Real
) : ( ( ) (
V24
()
V25
()
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) )
>
0
: ( ( ) (
Relation-like
non-empty
empty-yielding
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) )
-defined
RAT
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V136
()
V139
() )
set
)
-valued
V8
()
V12
()
empty
Function-like
one-to-one
constant
functional
V24
()
V25
()
V30
()
V31
()
finite
FinSequence-like
FinSubsequence-like
FinSequence-membered
ext-real
non
positive
non
negative
V123
()
V124
()
V125
()
V126
()
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V133
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
K48
(
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
Carrier
(
(
a
: ( ( ) (
V24
()
V25
()
ext-real
)
Real
)
*
L1
: ( (
convex
) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
quasi_total
V123
()
V124
()
V125
()
convex
)
Convex_Combination
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) )
)
: ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
quasi_total
V123
()
V124
()
V125
() )
Linear_Combination
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) )
+
(
b
: ( ( ) (
V24
()
V25
()
ext-real
)
Real
)
*
L2
: ( (
convex
) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
quasi_total
V123
()
V124
()
V125
()
convex
)
Convex_Combination
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) )
)
: ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
quasi_total
V123
()
V124
()
V125
() )
Linear_Combination
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) )
)
: ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
quasi_total
V123
()
V124
()
V125
() )
Linear_Combination
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) ) : ( ( ) (
finite
)
Element
of
K48
( the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
(
Carrier
(
a
: ( ( ) (
V24
()
V25
()
ext-real
)
Real
)
*
L1
: ( (
convex
) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
quasi_total
V123
()
V124
()
V125
()
convex
)
Convex_Combination
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) )
)
: ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
quasi_total
V123
()
V124
()
V125
() )
Linear_Combination
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) )
)
: ( ( ) (
finite
)
Element
of
K48
( the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
\/
(
Carrier
(
b
: ( ( ) (
V24
()
V25
()
ext-real
)
Real
)
*
L2
: ( (
convex
) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
quasi_total
V123
()
V124
()
V125
()
convex
)
Convex_Combination
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) )
)
: ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
quasi_total
V123
()
V124
()
V125
() )
Linear_Combination
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) )
)
: ( ( ) (
finite
)
Element
of
K48
( the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
K48
( the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: CONVEX2:13
for
F
,
G
being ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) st
F
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) ,
G
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
are_fiberwise_equipotent
holds
for
x1
,
x2
being ( ( ) ( )
set
) st
x1
: ( ( ) ( )
set
)
in
dom
F
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( ( ) ( )
set
) &
x2
: ( ( ) ( )
set
)
in
dom
F
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( ( ) ( )
set
) &
x1
: ( ( ) ( )
set
)
<>
x2
: ( ( ) ( )
set
) holds
ex
z1
,
z2
being ( ( ) ( )
set
) st
(
z1
: ( ( ) ( )
set
)
in
dom
G
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( ( ) ( )
set
) &
z2
: ( ( ) ( )
set
)
in
dom
G
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( ( ) ( )
set
) &
z1
: ( ( ) ( )
set
)
<>
z2
: ( ( ) ( )
set
) &
F
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
x1
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
=
G
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
z1
: ( ( ) ( )
set
) : ( ( ) ( )
set
) &
F
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
x2
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
=
G
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
z2
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
theorem
:: CONVEX2:14
for
V
being ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
)
for
L
being ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
quasi_total
V123
()
V124
()
V125
() )
Linear_Combination
of
V
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) )
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
c=
Carrier
L
: ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
quasi_total
V123
()
V124
()
V125
() )
Linear_Combination
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) ) : ( ( ) (
finite
)
Element
of
K48
( the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) holds
ex
L1
being ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
quasi_total
V123
()
V124
()
V125
() )
Linear_Combination
of
V
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) ) st
Carrier
L1
: ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
)
-defined
REAL
: ( ( ) ( non
empty
non
finite
V133
()
V134
()
V135
()
V139
() )
set
)
-valued
Function-like
quasi_total
V123
()
V124
()
V125
() )
Linear_Combination
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) ) : ( ( ) (
finite
)
Element
of
K48
( the
carrier
of
b
1
: ( ( non
empty
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
V73
()
V74
()
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V106
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
A
: ( ( ) ( )
Subset
of ) ;