:: Infimum and Supremum of the Set of Real Numbers. Measure Theory
:: by J\'ozef Bia{\l}as
::
:: Received September 27, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users
begin
definition
mode
R_eal
is
Element
of
ExtREAL
;
end;
definition
:: original:
+infty
redefine
func
+infty
->
R_eal
;
coherence
+infty
is
R_eal
by
XXREAL_0:def 1
;
:: original:
-infty
redefine
func
-infty
->
R_eal
;
coherence
-infty
is
R_eal
by
XXREAL_0:def 1
;
end;
::
:: Set of UpperBound and set of LowerBound of X being a subset of ExtREAL
::
definition
let
X
be
ext-real-membered
set
;
func
SetMajorant
X
->
ext-real-membered
set
means
:
Def1
:
:: SUPINF_1:def 1
for
x
being
ext-real
number
holds
(
x
in
it
iff
x
is
UpperBound
of
X
);
existence
ex
b
1
being
ext-real-membered
set
st
for
x
being
ext-real
number
holds
(
x
in
b
1
iff
x
is
UpperBound
of
X
)
proof
end;
uniqueness
for
b
1
,
b
2
being
ext-real-membered
set
st ( for
x
being
ext-real
number
holds
(
x
in
b
1
iff
x
is
UpperBound
of
X
) ) & ( for
x
being
ext-real
number
holds
(
x
in
b
2
iff
x
is
UpperBound
of
X
) ) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def1
defines
SetMajorant
SUPINF_1:def 1 :
for
X
,
b
2
being
ext-real-membered
set
holds
(
b
2
=
SetMajorant
X
iff for
x
being
ext-real
number
holds
(
x
in
b
2
iff
x
is
UpperBound
of
X
) );
registration
let
X
be
ext-real-membered
set
;
cluster
SetMajorant
X
->
non
empty
ext-real-membered
;
coherence
not
SetMajorant
X
is
empty
proof
end;
end;
theorem
:: SUPINF_1:1
for
X
,
Y
being
ext-real-membered
set
st
X
c=
Y
holds
for
x
being
ext-real
number
st
x
in
SetMajorant
Y
holds
x
in
SetMajorant
X
proof
end;
definition
let
X
be
ext-real-membered
set
;
func
SetMinorant
X
->
ext-real-membered
set
means
:
Def2
:
:: SUPINF_1:def 2
for
x
being
ext-real
number
holds
(
x
in
it
iff
x
is
LowerBound
of
X
);
existence
ex
b
1
being
ext-real-membered
set
st
for
x
being
ext-real
number
holds
(
x
in
b
1
iff
x
is
LowerBound
of
X
)
proof
end;
uniqueness
for
b
1
,
b
2
being
ext-real-membered
set
st ( for
x
being
ext-real
number
holds
(
x
in
b
1
iff
x
is
LowerBound
of
X
) ) & ( for
x
being
ext-real
number
holds
(
x
in
b
2
iff
x
is
LowerBound
of
X
) ) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def2
defines
SetMinorant
SUPINF_1:def 2 :
for
X
,
b
2
being
ext-real-membered
set
holds
(
b
2
=
SetMinorant
X
iff for
x
being
ext-real
number
holds
(
x
in
b
2
iff
x
is
LowerBound
of
X
) );
registration
let
X
be
ext-real-membered
set
;
cluster
SetMinorant
X
->
non
empty
ext-real-membered
;
coherence
not
SetMinorant
X
is
empty
proof
end;
end;
theorem
:: SUPINF_1:2
for
X
,
Y
being
ext-real-membered
set
st
X
c=
Y
holds
for
x
being
ext-real
number
st
x
in
SetMinorant
Y
holds
x
in
SetMinorant
X
proof
end;
::
:: sup X, inf X least upper bound and greatest lower bound of set X
::
theorem
:: SUPINF_1:3
for
X
being non
empty
ext-real-membered
set
holds
(
sup
X
=
inf
(
SetMajorant
X
)
&
inf
X
=
sup
(
SetMinorant
X
)
)
proof
end;
registration
let
X
be non
empty
set
;
cluster
non
empty
with_non-empty_elements
for
Element
of
K6
(
K6
(
X
));
existence
ex
b
1
being
Subset-Family
of
X
st
( not
b
1
is
empty
&
b
1
is
with_non-empty_elements
)
proof
end;
end;
definition
let
X
be non
empty
set
;
mode
bool_DOMAIN of
X
is
non
empty
with_non-empty_elements
Subset-Family
of
X
;
end;
definition
let
F
be
bool_DOMAIN
of
ExtREAL
;
func
SUP
F
->
ext-real-membered
set
means
:
Def3
:
:: SUPINF_1:def 3
for
a
being
ext-real
number
holds
(
a
in
it
iff ex
A
being non
empty
ext-real-membered
set
st
(
A
in
F
&
a
=
sup
A
) );
existence
ex
b
1
being
ext-real-membered
set
st
for
a
being
ext-real
number
holds
(
a
in
b
1
iff ex
A
being non
empty
ext-real-membered
set
st
(
A
in
F
&
a
=
sup
A
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
ext-real-membered
set
st ( for
a
being
ext-real
number
holds
(
a
in
b
1
iff ex
A
being non
empty
ext-real-membered
set
st
(
A
in
F
&
a
=
sup
A
) ) ) & ( for
a
being
ext-real
number
holds
(
a
in
b
2
iff ex
A
being non
empty
ext-real-membered
set
st
(
A
in
F
&
a
=
sup
A
) ) ) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def3
defines
SUP
SUPINF_1:def 3 :
for
F
being
bool_DOMAIN
of
ExtREAL
for
b
2
being
ext-real-membered
set
holds
(
b
2
=
SUP
F
iff for
a
being
ext-real
number
holds
(
a
in
b
2
iff ex
A
being non
empty
ext-real-membered
set
st
(
A
in
F
&
a
=
sup
A
) ) );
registration
let
F
be
bool_DOMAIN
of
ExtREAL
;
cluster
SUP
F
->
non
empty
ext-real-membered
;
coherence
not
SUP
F
is
empty
proof
end;
end;
theorem
Th4
:
:: SUPINF_1:4
for
F
being
bool_DOMAIN
of
ExtREAL
for
S
being non
empty
ext-real-membered
number
st
S
=
union
F
holds
sup
S
is
UpperBound
of
SUP
F
proof
end;
theorem
Th5
:
:: SUPINF_1:5
for
F
being
bool_DOMAIN
of
ExtREAL
for
S
being
ext-real-membered
set
st
S
=
union
F
holds
sup
(
SUP
F
)
is
UpperBound
of
S
proof
end;
theorem
:: SUPINF_1:6
for
F
being
bool_DOMAIN
of
ExtREAL
for
S
being non
empty
ext-real-membered
set
st
S
=
union
F
holds
sup
S
=
sup
(
SUP
F
)
proof
end;
definition
let
F
be
bool_DOMAIN
of
ExtREAL
;
func
INF
F
->
ext-real-membered
set
means
:
Def4
:
:: SUPINF_1:def 4
for
a
being
ext-real
number
holds
(
a
in
it
iff ex
A
being non
empty
ext-real-membered
set
st
(
A
in
F
&
a
=
inf
A
) );
existence
ex
b
1
being
ext-real-membered
set
st
for
a
being
ext-real
number
holds
(
a
in
b
1
iff ex
A
being non
empty
ext-real-membered
set
st
(
A
in
F
&
a
=
inf
A
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
ext-real-membered
set
st ( for
a
being
ext-real
number
holds
(
a
in
b
1
iff ex
A
being non
empty
ext-real-membered
set
st
(
A
in
F
&
a
=
inf
A
) ) ) & ( for
a
being
ext-real
number
holds
(
a
in
b
2
iff ex
A
being non
empty
ext-real-membered
set
st
(
A
in
F
&
a
=
inf
A
) ) ) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def4
defines
INF
SUPINF_1:def 4 :
for
F
being
bool_DOMAIN
of
ExtREAL
for
b
2
being
ext-real-membered
set
holds
(
b
2
=
INF
F
iff for
a
being
ext-real
number
holds
(
a
in
b
2
iff ex
A
being non
empty
ext-real-membered
set
st
(
A
in
F
&
a
=
inf
A
) ) );
registration
let
F
be
bool_DOMAIN
of
ExtREAL
;
cluster
INF
F
->
non
empty
ext-real-membered
;
coherence
not
INF
F
is
empty
proof
end;
end;
theorem
Th7
:
:: SUPINF_1:7
for
F
being
bool_DOMAIN
of
ExtREAL
for
S
being non
empty
ext-real-membered
set
st
S
=
union
F
holds
inf
S
is
LowerBound
of
INF
F
proof
end;
theorem
Th8
:
:: SUPINF_1:8
for
F
being
bool_DOMAIN
of
ExtREAL
for
S
being
ext-real-membered
set
st
S
=
union
F
holds
inf
(
INF
F
)
is
LowerBound
of
S
proof
end;
theorem
:: SUPINF_1:9
for
F
being
bool_DOMAIN
of
ExtREAL
for
S
being non
empty
ext-real-membered
set
st
S
=
union
F
holds
inf
S
=
inf
(
INF
F
)
proof
end;
:: Set of UpperBound and set of LowerBound of X being a subset of ExtREAL
::