:: SUPINF_1 semantic presentation
begin
definition
mode
R_eal
is
( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
)
set
) ) ;
end;
definition
:: original:
+infty
redefine
func
+infty
->
( ( ) (
ext-real
)
R_eal
) ;
:: original:
-infty
redefine
func
-infty
->
( ( ) (
ext-real
)
R_eal
) ;
end;
definition
let
X
be ( (
ext-real-membered
) (
ext-real-membered
)
set
) ;
func
SetMajorant
X
->
( (
ext-real-membered
) (
ext-real-membered
)
set
)
means
:: SUPINF_1:def 1
for
x
being ( (
ext-real
) (
ext-real
)
number
) holds
(
x
: ( (
ext-real
) (
ext-real
)
number
)
in
it
: ( (
ext-real
) (
ext-real
)
set
) iff
x
: ( (
ext-real
) (
ext-real
)
number
) is ( ( ) (
ext-real
)
UpperBound
of
X
: ( (
ext-real-membered
right_end
) (
ext-real-membered
right_end
)
set
) ) );
end;
registration
let
X
be ( (
ext-real-membered
) (
ext-real-membered
)
set
) ;
cluster
SetMajorant
X
: ( (
ext-real-membered
) (
ext-real-membered
)
set
) : ( (
ext-real-membered
) (
ext-real-membered
)
set
)
->
non
empty
ext-real-membered
;
end;
theorem
:: SUPINF_1:1
for
X
,
Y
being ( (
ext-real-membered
) (
ext-real-membered
)
set
) st
X
: ( (
ext-real-membered
) (
ext-real-membered
)
set
)
c=
Y
: ( (
ext-real-membered
) (
ext-real-membered
)
set
) holds
for
x
being ( (
ext-real
) (
ext-real
)
number
) st
x
: ( (
ext-real
) (
ext-real
)
number
)
in
SetMajorant
Y
: ( (
ext-real-membered
) (
ext-real-membered
)
set
) : ( (
ext-real-membered
) ( non
empty
ext-real-membered
)
set
) holds
x
: ( (
ext-real
) (
ext-real
)
number
)
in
SetMajorant
X
: ( (
ext-real-membered
) (
ext-real-membered
)
set
) : ( (
ext-real-membered
) ( non
empty
ext-real-membered
)
set
) ;
definition
let
X
be ( (
ext-real-membered
) (
ext-real-membered
)
set
) ;
func
SetMinorant
X
->
( (
ext-real-membered
) (
ext-real-membered
)
set
)
means
:: SUPINF_1:def 2
for
x
being ( (
ext-real
) (
ext-real
)
number
) holds
(
x
: ( (
ext-real
) (
ext-real
)
number
)
in
it
: ( (
ext-real
) (
ext-real
)
set
) iff
x
: ( (
ext-real
) (
ext-real
)
number
) is ( ( ) (
ext-real
)
LowerBound
of
X
: ( (
V2
() ) (
V2
() )
set
) ) );
end;
registration
let
X
be ( (
ext-real-membered
) (
ext-real-membered
)
set
) ;
cluster
SetMinorant
X
: ( (
ext-real-membered
) (
ext-real-membered
)
set
) : ( (
ext-real-membered
) (
ext-real-membered
)
set
)
->
non
empty
ext-real-membered
;
end;
theorem
:: SUPINF_1:2
for
X
,
Y
being ( (
ext-real-membered
) (
ext-real-membered
)
set
) st
X
: ( (
ext-real-membered
) (
ext-real-membered
)
set
)
c=
Y
: ( (
ext-real-membered
) (
ext-real-membered
)
set
) holds
for
x
being ( (
ext-real
) (
ext-real
)
number
) st
x
: ( (
ext-real
) (
ext-real
)
number
)
in
SetMinorant
Y
: ( (
ext-real-membered
) (
ext-real-membered
)
set
) : ( (
ext-real-membered
) ( non
empty
ext-real-membered
)
set
) holds
x
: ( (
ext-real
) (
ext-real
)
number
)
in
SetMinorant
X
: ( (
ext-real-membered
) (
ext-real-membered
)
set
) : ( (
ext-real-membered
) ( non
empty
ext-real-membered
)
set
) ;
theorem
:: SUPINF_1:3
for
X
being ( ( non
empty
ext-real-membered
) ( non
empty
ext-real-membered
)
set
) holds
(
sup
X
: ( ( non
empty
ext-real-membered
) ( non
empty
ext-real-membered
)
set
) : ( (
ext-real
) (
ext-real
)
set
)
=
inf
(
SetMajorant
X
: ( ( non
empty
ext-real-membered
) ( non
empty
ext-real-membered
)
set
)
)
: ( (
ext-real-membered
) ( non
empty
ext-real-membered
)
set
) : ( (
ext-real
) (
ext-real
)
set
) &
inf
X
: ( ( non
empty
ext-real-membered
) ( non
empty
ext-real-membered
)
set
) : ( (
ext-real
) (
ext-real
)
set
)
=
sup
(
SetMinorant
X
: ( ( non
empty
ext-real-membered
) ( non
empty
ext-real-membered
)
set
)
)
: ( (
ext-real-membered
) ( non
empty
ext-real-membered
)
set
) : ( (
ext-real
) (
ext-real
)
set
) ) ;
registration
let
X
be ( ( non
empty
) ( non
empty
)
set
) ;
cluster
non
empty
with_non-empty_elements
for ( ( ) ( )
Element
of
K6
(
K6
(
X
: ( ( non
empty
) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
end;
definition
let
X
be ( ( non
empty
) ( non
empty
)
set
) ;
mode
bool_DOMAIN of
X
is
( ( non
empty
with_non-empty_elements
) ( non
empty
with_non-empty_elements
)
Subset-Family
of ) ;
end;
definition
let
F
be ( ( non
empty
with_non-empty_elements
) ( non
empty
with_non-empty_elements
)
bool_DOMAIN
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
)
set
) ) ;
func
SUP
F
->
( (
ext-real-membered
) (
ext-real-membered
)
set
)
means
:: SUPINF_1:def 3
for
a
being ( (
ext-real
) (
ext-real
)
number
) holds
(
a
: ( (
ext-real
) (
ext-real
)
number
)
in
it
: ( (
ext-real
) (
ext-real
)
set
) iff ex
A
being ( ( non
empty
ext-real-membered
) ( non
empty
ext-real-membered
)
set
) st
(
A
: ( ( non
empty
ext-real-membered
) ( non
empty
ext-real-membered
)
set
)
in
F
: ( ( non
empty
) ( non
empty
)
set
) &
a
: ( (
ext-real
) (
ext-real
)
number
)
=
sup
A
: ( ( non
empty
ext-real-membered
) ( non
empty
ext-real-membered
)
set
) : ( (
ext-real
) (
ext-real
)
set
) ) );
end;
registration
let
F
be ( ( non
empty
with_non-empty_elements
) ( non
empty
with_non-empty_elements
)
bool_DOMAIN
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
)
set
) ) ;
cluster
SUP
F
: ( ( non
empty
with_non-empty_elements
) ( non
empty
with_non-empty_elements
)
Element
of
K6
(
K6
(
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( (
ext-real-membered
) (
ext-real-membered
)
set
)
->
non
empty
ext-real-membered
;
end;
theorem
:: SUPINF_1:4
for
F
being ( ( non
empty
with_non-empty_elements
) ( non
empty
with_non-empty_elements
)
bool_DOMAIN
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
)
set
) )
for
S
being ( ( non
empty
ext-real-membered
) ( non
empty
ext-real-membered
)
number
) st
S
: ( ( non
empty
ext-real-membered
) ( non
empty
ext-real-membered
)
number
)
=
union
F
: ( ( non
empty
with_non-empty_elements
) ( non
empty
with_non-empty_elements
)
bool_DOMAIN
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
)
set
) ) : ( ( ) (
ext-real-membered
)
Element
of
K6
(
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
)
set
) ) : ( ( ) ( non
empty
)
set
) ) holds
sup
S
: ( ( non
empty
ext-real-membered
) ( non
empty
ext-real-membered
)
number
) : ( (
ext-real
) (
ext-real
)
set
) is ( ( ) (
ext-real
)
UpperBound
of
SUP
F
: ( ( non
empty
with_non-empty_elements
) ( non
empty
with_non-empty_elements
)
bool_DOMAIN
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
)
set
) ) : ( (
ext-real-membered
) ( non
empty
ext-real-membered
)
set
) ) ;
theorem
:: SUPINF_1:5
for
F
being ( ( non
empty
with_non-empty_elements
) ( non
empty
with_non-empty_elements
)
bool_DOMAIN
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
)
set
) )
for
S
being ( (
ext-real-membered
) (
ext-real-membered
)
set
) st
S
: ( (
ext-real-membered
) (
ext-real-membered
)
set
)
=
union
F
: ( ( non
empty
with_non-empty_elements
) ( non
empty
with_non-empty_elements
)
bool_DOMAIN
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
)
set
) ) : ( ( ) (
ext-real-membered
)
Element
of
K6
(
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
)
set
) ) : ( ( ) ( non
empty
)
set
) ) holds
sup
(
SUP
F
: ( ( non
empty
with_non-empty_elements
) ( non
empty
with_non-empty_elements
)
bool_DOMAIN
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
)
set
) )
)
: ( (
ext-real-membered
) ( non
empty
ext-real-membered
)
set
) : ( (
ext-real
) (
ext-real
)
set
) is ( ( ) (
ext-real
)
UpperBound
of
S
: ( (
ext-real-membered
) (
ext-real-membered
)
set
) ) ;
theorem
:: SUPINF_1:6
for
F
being ( ( non
empty
with_non-empty_elements
) ( non
empty
with_non-empty_elements
)
bool_DOMAIN
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
)
set
) )
for
S
being ( ( non
empty
ext-real-membered
) ( non
empty
ext-real-membered
)
set
) st
S
: ( ( non
empty
ext-real-membered
) ( non
empty
ext-real-membered
)
set
)
=
union
F
: ( ( non
empty
with_non-empty_elements
) ( non
empty
with_non-empty_elements
)
bool_DOMAIN
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
)
set
) ) : ( ( ) (
ext-real-membered
)
Element
of
K6
(
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
)
set
) ) : ( ( ) ( non
empty
)
set
) ) holds
sup
S
: ( ( non
empty
ext-real-membered
) ( non
empty
ext-real-membered
)
set
) : ( (
ext-real
) (
ext-real
)
set
)
=
sup
(
SUP
F
: ( ( non
empty
with_non-empty_elements
) ( non
empty
with_non-empty_elements
)
bool_DOMAIN
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
)
set
) )
)
: ( (
ext-real-membered
) ( non
empty
ext-real-membered
)
set
) : ( (
ext-real
) (
ext-real
)
set
) ;
definition
let
F
be ( ( non
empty
with_non-empty_elements
) ( non
empty
with_non-empty_elements
)
bool_DOMAIN
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
)
set
) ) ;
func
INF
F
->
( (
ext-real-membered
) (
ext-real-membered
)
set
)
means
:: SUPINF_1:def 4
for
a
being ( (
ext-real
) (
ext-real
)
number
) holds
(
a
: ( (
ext-real
) (
ext-real
)
number
)
in
it
: ( (
ext-real
) (
ext-real
)
set
) iff ex
A
being ( ( non
empty
ext-real-membered
) ( non
empty
ext-real-membered
)
set
) st
(
A
: ( ( non
empty
ext-real-membered
) ( non
empty
ext-real-membered
)
set
)
in
F
: ( ( non
empty
) ( non
empty
)
set
) &
a
: ( (
ext-real
) (
ext-real
)
number
)
=
inf
A
: ( ( non
empty
ext-real-membered
) ( non
empty
ext-real-membered
)
set
) : ( (
ext-real
) (
ext-real
)
set
) ) );
end;
registration
let
F
be ( ( non
empty
with_non-empty_elements
) ( non
empty
with_non-empty_elements
)
bool_DOMAIN
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
)
set
) ) ;
cluster
INF
F
: ( ( non
empty
with_non-empty_elements
) ( non
empty
with_non-empty_elements
)
Element
of
K6
(
K6
(
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( (
ext-real-membered
) (
ext-real-membered
)
set
)
->
non
empty
ext-real-membered
;
end;
theorem
:: SUPINF_1:7
for
F
being ( ( non
empty
with_non-empty_elements
) ( non
empty
with_non-empty_elements
)
bool_DOMAIN
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
)
set
) )
for
S
being ( ( non
empty
ext-real-membered
) ( non
empty
ext-real-membered
)
set
) st
S
: ( ( non
empty
ext-real-membered
) ( non
empty
ext-real-membered
)
set
)
=
union
F
: ( ( non
empty
with_non-empty_elements
) ( non
empty
with_non-empty_elements
)
bool_DOMAIN
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
)
set
) ) : ( ( ) (
ext-real-membered
)
Element
of
K6
(
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
)
set
) ) : ( ( ) ( non
empty
)
set
) ) holds
inf
S
: ( ( non
empty
ext-real-membered
) ( non
empty
ext-real-membered
)
set
) : ( (
ext-real
) (
ext-real
)
set
) is ( ( ) (
ext-real
)
LowerBound
of
INF
F
: ( ( non
empty
with_non-empty_elements
) ( non
empty
with_non-empty_elements
)
bool_DOMAIN
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
)
set
) ) : ( (
ext-real-membered
) ( non
empty
ext-real-membered
)
set
) ) ;
theorem
:: SUPINF_1:8
for
F
being ( ( non
empty
with_non-empty_elements
) ( non
empty
with_non-empty_elements
)
bool_DOMAIN
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
)
set
) )
for
S
being ( (
ext-real-membered
) (
ext-real-membered
)
set
) st
S
: ( (
ext-real-membered
) (
ext-real-membered
)
set
)
=
union
F
: ( ( non
empty
with_non-empty_elements
) ( non
empty
with_non-empty_elements
)
bool_DOMAIN
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
)
set
) ) : ( ( ) (
ext-real-membered
)
Element
of
K6
(
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
)
set
) ) : ( ( ) ( non
empty
)
set
) ) holds
inf
(
INF
F
: ( ( non
empty
with_non-empty_elements
) ( non
empty
with_non-empty_elements
)
bool_DOMAIN
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
)
set
) )
)
: ( (
ext-real-membered
) ( non
empty
ext-real-membered
)
set
) : ( (
ext-real
) (
ext-real
)
set
) is ( ( ) (
ext-real
)
LowerBound
of
S
: ( (
ext-real-membered
) (
ext-real-membered
)
set
) ) ;
theorem
:: SUPINF_1:9
for
F
being ( ( non
empty
with_non-empty_elements
) ( non
empty
with_non-empty_elements
)
bool_DOMAIN
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
)
set
) )
for
S
being ( ( non
empty
ext-real-membered
) ( non
empty
ext-real-membered
)
set
) st
S
: ( ( non
empty
ext-real-membered
) ( non
empty
ext-real-membered
)
set
)
=
union
F
: ( ( non
empty
with_non-empty_elements
) ( non
empty
with_non-empty_elements
)
bool_DOMAIN
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
)
set
) ) : ( ( ) (
ext-real-membered
)
Element
of
K6
(
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
)
set
) ) : ( ( ) ( non
empty
)
set
) ) holds
inf
S
: ( ( non
empty
ext-real-membered
) ( non
empty
ext-real-membered
)
set
) : ( (
ext-real
) (
ext-real
)
set
)
=
inf
(
INF
F
: ( ( non
empty
with_non-empty_elements
) ( non
empty
with_non-empty_elements
)
bool_DOMAIN
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
)
set
) )
)
: ( (
ext-real-membered
) ( non
empty
ext-real-membered
)
set
) : ( (
ext-real
) (
ext-real
)
set
) ;