inf (proj1 | (LSeg |[0 ,1]|,|[1,1]|)) = 0
proof
set X =
LSeg |[0 ,1]|,
|[1,1]|;
reconsider Z =
(proj1 | (LSeg |[0 ,1]|,|[1,1]|)) .: the
carrier of
((TOP-REAL 2) | (LSeg |[0 ,1]|,|[1,1]|)) as
Subset of
REAL ;
A1:
LSeg |[0 ,1]|,
|[1,1]| =
[#] ((TOP-REAL 2) | (LSeg |[0 ,1]|,|[1,1]|))
by PRE_TOPC:def 10
.=
the
carrier of
((TOP-REAL 2) | (LSeg |[0 ,1]|,|[1,1]|))
;
A2:
for
p being
real number st
p in Z holds
p >= 0
proof
let p be
real number ;
:: thesis: ( p in Z implies p >= 0 )
assume
p in Z
;
:: thesis: p >= 0
then consider p0 being
set such that A3:
p0 in the
carrier of
((TOP-REAL 2) | (LSeg |[0 ,1]|,|[1,1]|))
and
p0 in the
carrier of
((TOP-REAL 2) | (LSeg |[0 ,1]|,|[1,1]|))
and A4:
p = (proj1 | (LSeg |[0 ,1]|,|[1,1]|)) . p0
by FUNCT_2:115;
reconsider p0 =
p0 as
Point of
(TOP-REAL 2) by A1, A3;
(
|[0 ,1]| `1 = 0 &
|[1,1]| `1 = 1 )
by EUCLID:56;
then
p0 `1 >= 0
by A1, A3, TOPREAL1:9;
hence
p >= 0
by A1, A3, A4, PSCOMP_1:69;
:: thesis: verum
end;
for
q being
real number st ( for
p being
real number st
p in Z holds
p >= q ) holds
0 >= q
proof
let q be
real number ;
:: thesis: ( ( for p being real number st p in Z holds
p >= q ) implies 0 >= q )
assume A5:
for
p being
real number st
p in Z holds
p >= q
;
:: thesis: 0 >= q
A6:
|[0 ,1]| in LSeg |[0 ,1]|,
|[1,1]|
by RLTOPSP1:69;
then (proj1 | (LSeg |[0 ,1]|,|[1,1]|)) . |[0 ,1]| =
|[0 ,1]| `1
by PSCOMP_1:69
.=
0
by EUCLID:56
;
hence
0 >= q
by A1, A5, A6, FUNCT_2:43;
:: thesis: verum
end;
hence
inf (proj1 | (LSeg |[0 ,1]|,|[1,1]|)) = 0
by A2, SEQ_4:61;
:: thesis: verum
end;
hence
N-min R^2-unit_square = |[0 ,1]|
by Th35, Th39; :: thesis: verum