REAL is non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval set
NAT is ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below Element of K32(REAL)
K32(REAL) is non empty non trivial non finite set
K597() is TopSpace-like T_0 T_1 T_2 compact real-membered V241() SubSpace of R^1
R^1 is non empty strict TopSpace-like T_0 T_1 T_2 real-membered TopStruct
the carrier of K597() is complex-membered ext-real-membered real-membered set
K575(K597(),K597()) is strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of K575(K597(),K597()) is set
omega is ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below set
K32(omega) is non empty non trivial non finite set
K33(NAT,REAL) is Relation-like non trivial non finite V124() V125() V126() set
K32(K33(NAT,REAL)) is non empty non trivial non finite set
K32(K32(REAL)) is non empty non trivial non finite set
COMPLEX is non empty non trivial non finite complex-membered V123() set
RAT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered V123() set
INT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered integer-membered V123() set
K33(COMPLEX,COMPLEX) is Relation-like non empty non trivial non finite V124() set
K32(K33(COMPLEX,COMPLEX)) is non empty non trivial non finite set
K33(K33(COMPLEX,COMPLEX),COMPLEX) is Relation-like non empty non trivial non finite V124() set
K32(K33(K33(COMPLEX,COMPLEX),COMPLEX)) is non empty non trivial non finite set
K33(REAL,REAL) is Relation-like non empty non trivial non finite V124() V125() V126() set
K32(K33(REAL,REAL)) is non empty non trivial non finite set
K33(K33(REAL,REAL),REAL) is Relation-like non empty non trivial non finite V124() V125() V126() set
K32(K33(K33(REAL,REAL),REAL)) is non empty non trivial non finite set
K33(RAT,RAT) is Relation-like RAT -valued non empty non trivial non finite V124() V125() V126() set
K32(K33(RAT,RAT)) is non empty non trivial non finite set
K33(K33(RAT,RAT),RAT) is Relation-like RAT -valued non empty non trivial non finite V124() V125() V126() set
K32(K33(K33(RAT,RAT),RAT)) is non empty non trivial non finite set
K33(INT,INT) is Relation-like RAT -valued INT -valued non empty non trivial non finite V124() V125() V126() set
K32(K33(INT,INT)) is non empty non trivial non finite set
K33(K33(INT,INT),INT) is Relation-like RAT -valued INT -valued non empty non trivial non finite V124() V125() V126() set
K32(K33(K33(INT,INT),INT)) is non empty non trivial non finite set
K33(NAT,NAT) is Relation-like RAT -valued INT -valued V124() V125() V126() V127() set
K33(K33(NAT,NAT),NAT) is Relation-like RAT -valued INT -valued V124() V125() V126() V127() set
K32(K33(K33(NAT,NAT),NAT)) is non empty set
K32(NAT) is non empty non trivial non finite set
K276() is set
1 is ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of NAT
ExtREAL is non empty ext-real-membered interval set
K33(1,1) is Relation-like RAT -valued INT -valued non empty finite V124() V125() V126() V127() set
K32(K33(1,1)) is non empty finite V43() set
K33(K33(1,1),1) is Relation-like RAT -valued INT -valued non empty finite V124() V125() V126() V127() set
K32(K33(K33(1,1),1)) is non empty finite V43() set
K33(K33(1,1),REAL) is Relation-like non empty non trivial non finite V124() V125() V126() set
K32(K33(K33(1,1),REAL)) is non empty non trivial non finite set
2 is ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of NAT
K33(2,2) is Relation-like RAT -valued INT -valued non empty finite V124() V125() V126() V127() set
K33(K33(2,2),REAL) is Relation-like non empty non trivial non finite V124() V125() V126() set
K32(K33(K33(2,2),REAL)) is non empty non trivial non finite set
K519(2) is V216() L15()
the carrier of K519(2) is set
K590() is T_0 T_1 T_2 compact real-membered V241() TopStruct
the carrier of K590() is complex-membered ext-real-membered real-membered set
RealSpace is non empty strict Reflexive discerning symmetric triangle Discerning real-membered MetrStruct
R^1 is non empty strict TopSpace-like T_0 T_1 T_2 connected real-membered interval V241() SubSpace of R^1
the carrier of R^1 is non empty complex-membered ext-real-membered real-membered set
K32( the carrier of R^1) is non empty set
K32(K32( the carrier of R^1)) is non empty set
K608(2) is non empty compact V240() V241() SubSpace of K519(2)
the carrier of K608(2) is non empty set
K33( the carrier of R^1, the carrier of K608(2)) is Relation-like non empty set
K32(K33( the carrier of R^1, the carrier of K608(2))) is non empty set
K612() is Relation-like Function-like V27( the carrier of R^1, the carrier of K608(2)) V27( the carrier of R^1, the carrier of K608(2)) V28( the carrier of K608(2)) continuous Element of K32(K33( the carrier of R^1, the carrier of K608(2)))
K609() is Element of the carrier of K608(2)
K611(K609()) is non empty strict SubSpace of K608(2)
the carrier of K611(K609()) is non empty set
0 is Relation-like non-empty empty-yielding RAT -valued functional ordinal natural empty ext-real non positive non negative finite finite-yielding V43() cardinal {} -element real V65() V66() V67() FinSequence-like FinSequence-membered complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() V124() V125() V126() V127() bounded_below bounded_above real-bounded interval Element of NAT
{} is Relation-like non-empty empty-yielding RAT -valued functional ordinal natural empty ext-real non positive non negative finite finite-yielding V43() cardinal {} -element real V65() V66() FinSequence-like FinSequence-membered complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() V124() V125() V126() V127() bounded_below bounded_above real-bounded interval set
the Relation-like non-empty empty-yielding RAT -valued functional ordinal natural empty ext-real non positive non negative finite finite-yielding V43() cardinal {} -element real V65() V66() FinSequence-like FinSequence-membered complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() V124() V125() V126() V127() bounded_below bounded_above real-bounded interval set is Relation-like non-empty empty-yielding RAT -valued functional ordinal natural empty ext-real non positive non negative finite finite-yielding V43() cardinal {} -element real V65() V66() FinSequence-like FinSequence-membered complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() V124() V125() V126() V127() bounded_below bounded_above real-bounded interval set
].0,1.[ is non empty complex-membered ext-real-membered real-membered open non left_end non right_end interval Element of K32(REAL)
R^1 ].0,1.[ is non empty open complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
R^1 | (R^1 ].0,1.[) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (R^1 | (R^1 ].0,1.[)) is non empty complex-membered ext-real-membered real-membered set
K33( the carrier of K611(K609()), the carrier of (R^1 | (R^1 ].0,1.[))) is Relation-like non empty V124() V125() V126() set
K32(K33( the carrier of K611(K609()), the carrier of (R^1 | (R^1 ].0,1.[)))) is non empty set
K610() is Element of the carrier of K608(2)
K611(K610()) is non empty strict SubSpace of K608(2)
the carrier of K611(K610()) is non empty set
1 / 2 is ext-real non negative real V65() Element of REAL
3 is ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of NAT
3 / 2 is ext-real non negative real V65() Element of REAL
].(1 / 2),(3 / 2).[ is non empty complex-membered ext-real-membered real-membered open non left_end non right_end interval Element of K32(REAL)
R^1 ].(1 / 2),(3 / 2).[ is non empty open complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
R^1 | (R^1 ].(1 / 2),(3 / 2).[) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (R^1 | (R^1 ].(1 / 2),(3 / 2).[)) is non empty complex-membered ext-real-membered real-membered set
K33( the carrier of K611(K610()), the carrier of (R^1 | (R^1 ].(1 / 2),(3 / 2).[))) is Relation-like non empty V124() V125() V126() set
K32(K33( the carrier of K611(K610()), the carrier of (R^1 | (R^1 ].(1 / 2),(3 / 2).[)))) is non empty set
{{},1} is non empty finite V43() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded set
K33( the carrier of K597(), the carrier of K597()) is Relation-like V124() V125() V126() set
K32(K33( the carrier of K597(), the carrier of K597())) is non empty set
K32( the carrier of K575(K597(),K597())) is non empty set
K33(COMPLEX,REAL) is Relation-like non empty non trivial non finite V124() V125() V126() set
K32(K33(COMPLEX,REAL)) is non empty non trivial non finite set
the carrier of R^1 is non empty complex-membered ext-real-membered real-membered set
dom {} is Relation-like non-empty empty-yielding RAT -valued functional ordinal natural empty ext-real non positive non negative finite finite-yielding V43() cardinal {} -element real V65() V66() FinSequence-like FinSequence-membered complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() V124() V125() V126() V127() bounded_below bounded_above real-bounded interval set
rng {} is Relation-like non-empty empty-yielding RAT -valued functional ordinal natural empty ext-real non positive non negative finite finite-yielding V43() cardinal {} -element real V65() V66() FinSequence-like FinSequence-membered complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() V124() V125() V126() V127() bounded_below bounded_above real-bounded interval set
union {} is finite set
K32( the carrier of R^1) is non empty set
Seg 1 is non empty trivial finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of K32(NAT)
{1} is non empty trivial finite V43() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded set
Seg 2 is non empty finite 2 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of K32(NAT)
{1,2} is non empty finite V43() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded set
+infty is non empty ext-real positive non negative non real set
-infty is non empty ext-real non positive negative non real set
r is non empty set
[#] r is non empty non proper Element of K32(r)
K32(r) is non empty set
r is Reflexive discerning symmetric triangle SubSpace of RealSpace
the carrier of r is set
the carrier of RealSpace is non empty complex-membered ext-real-membered real-membered set
K32( the carrier of RealSpace) is non empty set
r is non empty complex-membered ext-real-membered real-membered bounded_below set
lower_bound r is ext-real real V65() set
inf r is ext-real real V65() set
s is complex-membered ext-real-membered real-membered closed Element of K32(REAL)
n is non empty complex-membered ext-real-membered real-membered bounded_below Element of K32(REAL)
lower_bound n is ext-real real V65() Element of REAL
inf n is ext-real real V65() set
Cl n is non empty complex-membered ext-real-membered real-membered closed bounded_below Element of K32(REAL)
lower_bound (Cl n) is ext-real real V65() Element of REAL
inf (Cl n) is ext-real real V65() set
r is non empty complex-membered ext-real-membered real-membered bounded_above set
upper_bound r is ext-real real V65() set
sup r is ext-real real V65() set
s is complex-membered ext-real-membered real-membered closed Element of K32(REAL)
n is non empty complex-membered ext-real-membered real-membered bounded_above Element of K32(REAL)
upper_bound n is ext-real real V65() Element of REAL
sup n is ext-real real V65() set
Cl n is non empty complex-membered ext-real-membered real-membered closed bounded_above Element of K32(REAL)
upper_bound (Cl n) is ext-real real V65() Element of REAL
sup (Cl n) is ext-real real V65() set
r is complex-membered ext-real-membered real-membered Element of K32(REAL)
s is complex-membered ext-real-membered real-membered Element of K32(REAL)
r \/ s is complex-membered ext-real-membered real-membered Element of K32(REAL)
Cl (r \/ s) is complex-membered ext-real-membered real-membered closed Element of K32(REAL)
Cl r is complex-membered ext-real-membered real-membered closed Element of K32(REAL)
Cl s is complex-membered ext-real-membered real-membered closed Element of K32(REAL)
(Cl r) \/ (Cl s) is complex-membered ext-real-membered real-membered Element of K32(REAL)
n is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
F is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
n \/ F is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
Cl (n \/ F) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
Cl n is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
Cl F is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
(Cl n) \/ (Cl F) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
(Cl r) \/ (Cl F) is complex-membered ext-real-membered real-membered set
r is ext-real real V65() set
s is ext-real set
[.r,s.[ is complex-membered ext-real-membered real-membered non right_end interval Element of K32(REAL)
n is ext-real set
].s,r.] is complex-membered ext-real-membered real-membered non left_end interval Element of K32(REAL)
n is ext-real set
r is ext-real real V65() set
s is ext-real real V65() set
[.r,s.[ is complex-membered ext-real-membered real-membered non right_end bounded_below interval Element of K32(REAL)
n is ext-real set
].r,s.] is complex-membered ext-real-membered real-membered non left_end bounded_above interval Element of K32(REAL)
n is ext-real set
].r,s.[ is complex-membered ext-real-membered real-membered open non left_end non right_end interval Element of K32(REAL)
n is ext-real set
n is ext-real set
r is ext-real real V65() set
s is ext-real real V65() set
[.r,s.[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
lower_bound [.r,s.[ is ext-real real V65() Element of REAL
F is ext-real real V65() set
r + s is ext-real real V65() set
(r + s) / 2 is ext-real real V65() Element of REAL
F is ext-real real V65() set
r + F is ext-real real V65() set
r + (r + F) is ext-real real V65() set
(r + (r + F)) / 2 is ext-real real V65() Element of REAL
r is ext-real real V65() set
s is ext-real real V65() set
[.r,s.[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
upper_bound [.r,s.[ is ext-real real V65() Element of REAL
F is ext-real real V65() set
r + s is ext-real real V65() set
(r + s) / 2 is ext-real real V65() Element of REAL
F is ext-real real V65() set
s - F is ext-real real V65() set
s - 0 is ext-real real V65() Element of REAL
s + (s - F) is ext-real real V65() set
(s + (s - F)) / 2 is ext-real real V65() Element of REAL
r is ext-real real V65() set
s is ext-real real V65() set
].r,s.] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
lower_bound ].r,s.] is ext-real real V65() Element of REAL
F is ext-real real V65() set
r + s is ext-real real V65() set
(r + s) / 2 is ext-real real V65() Element of REAL
F is ext-real real V65() set
r + F is ext-real real V65() set
r + (r + F) is ext-real real V65() set
(r + (r + F)) / 2 is ext-real real V65() Element of REAL
r is ext-real real V65() set
s is ext-real real V65() set
].r,s.] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
upper_bound ].r,s.] is ext-real real V65() Element of REAL
F is ext-real real V65() set
r + s is ext-real real V65() set
(r + s) / 2 is ext-real real V65() Element of REAL
F is ext-real real V65() set
s - F is ext-real real V65() set
s - 0 is ext-real real V65() Element of REAL
s + (s - F) is ext-real real V65() set
(s + (s - F)) / 2 is ext-real real V65() Element of REAL
r is ext-real real V65() set
left_closed_halfline r is complex-membered ext-real-membered real-membered closed Element of K32(REAL)
].-infty,r.] is complex-membered ext-real-membered real-membered non left_end bounded_above interval set
s is ext-real real V65() set
[.r,s.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
right_closed_halfline s is complex-membered ext-real-membered real-membered closed Element of K32(REAL)
[.s,+infty.[ is complex-membered ext-real-membered real-membered non right_end bounded_below interval set
(left_closed_halfline r) \/ (right_closed_halfline s) is complex-membered ext-real-membered real-membered Element of K32(REAL)
[.r,s.] /\ ((left_closed_halfline r) \/ (right_closed_halfline s)) is complex-membered ext-real-membered real-membered Element of K32(REAL)
{r,s} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
C is set
G is ext-real real V65() Element of REAL
C is set
r is ext-real real V65() set
left_open_halfline r is complex-membered ext-real-membered real-membered open Element of K32(REAL)
].-infty,r.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set
s is ext-real real V65() set
n is ext-real real V65() set
r - 0 is ext-real real V65() Element of REAL
r - 1 is ext-real real V65() Element of REAL
(r - 1) - 0 is ext-real real V65() Element of REAL
s - 1 is ext-real real V65() Element of REAL
s - 0 is ext-real real V65() Element of REAL
r is ext-real real V65() set
right_open_halfline r is complex-membered ext-real-membered real-membered open Element of K32(REAL)
].r,+infty.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set
s is ext-real real V65() set
r + 1 is ext-real real V65() Element of REAL
r + 0 is ext-real real V65() Element of REAL
(r + 1) + 0 is ext-real real V65() Element of REAL
s + 1 is ext-real real V65() Element of REAL
s + 0 is ext-real real V65() Element of REAL
r is ext-real real V65() set
left_closed_halfline r is complex-membered ext-real-membered real-membered closed Element of K32(REAL)
].-infty,r.] is complex-membered ext-real-membered real-membered non left_end bounded_above interval set
left_open_halfline r is complex-membered ext-real-membered real-membered open Element of K32(REAL)
].-infty,r.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set
n is ext-real set
F is ext-real set
[.n,F.] is ext-real-membered interval set
L is set
C is ext-real real V65() Element of REAL
G is ext-real real V65() Element of REAL
[.C,G.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
k is ext-real real V65() Element of REAL
left_open_halfline r is complex-membered ext-real-membered real-membered open Element of K32(REAL)
].-infty,r.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set
n is ext-real set
n is ext-real set
F is ext-real set
[.n,F.] is ext-real-membered interval set
L is set
C is ext-real real V65() Element of REAL
G is ext-real real V65() Element of REAL
[.C,G.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
k is ext-real real V65() Element of REAL
right_closed_halfline r is complex-membered ext-real-membered real-membered closed Element of K32(REAL)
[.r,+infty.[ is complex-membered ext-real-membered real-membered non right_end bounded_below interval set
right_open_halfline r is complex-membered ext-real-membered real-membered open Element of K32(REAL)
].r,+infty.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set
n is ext-real set
F is ext-real set
[.n,F.] is ext-real-membered interval set
L is set
C is ext-real real V65() Element of REAL
G is ext-real real V65() Element of REAL
[.C,G.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
k is ext-real real V65() Element of REAL
right_open_halfline r is complex-membered ext-real-membered real-membered open Element of K32(REAL)
].r,+infty.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set
n is ext-real set
n is ext-real set
F is ext-real set
[.n,F.] is ext-real-membered interval set
L is set
C is ext-real real V65() Element of REAL
G is ext-real real V65() Element of REAL
[.C,G.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
k is ext-real real V65() Element of REAL
r is ext-real real V65() set
left_closed_halfline r is complex-membered ext-real-membered real-membered closed non bounded_below bounded_above interval Element of K32(REAL)
].-infty,r.] is complex-membered ext-real-membered real-membered non left_end bounded_above interval set
upper_bound (left_closed_halfline r) is ext-real real V65() Element of REAL
n is ext-real real V65() set
r - n is ext-real real V65() set
r - 0 is ext-real real V65() Element of REAL
n is ext-real real V65() set
r is ext-real real V65() set
left_open_halfline r is complex-membered ext-real-membered real-membered open non bounded_below bounded_above interval Element of K32(REAL)
].-infty,r.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set
upper_bound (left_open_halfline r) is ext-real real V65() Element of REAL
n is ext-real real V65() set
r - n is ext-real real V65() set
r - 0 is ext-real real V65() Element of REAL
(r - n) + r is ext-real real V65() set
((r - n) + r) / 2 is ext-real real V65() Element of REAL
n is ext-real real V65() set
r is ext-real real V65() set
right_closed_halfline r is complex-membered ext-real-membered real-membered closed bounded_below non bounded_above interval Element of K32(REAL)
[.r,+infty.[ is complex-membered ext-real-membered real-membered non right_end bounded_below interval set
lower_bound (right_closed_halfline r) is ext-real real V65() Element of REAL
n is ext-real real V65() set
r + n is ext-real real V65() set
r + 0 is ext-real real V65() Element of REAL
n is ext-real real V65() set
r is ext-real real V65() set
right_open_halfline r is complex-membered ext-real-membered real-membered open bounded_below non bounded_above interval Element of K32(REAL)
].r,+infty.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set
lower_bound (right_open_halfline r) is ext-real real V65() Element of REAL
n is ext-real real V65() set
r + n is ext-real real V65() set
r + 0 is ext-real real V65() Element of REAL
r + r is ext-real real V65() set
(r + r) + n is ext-real real V65() set
((r + r) + n) / 2 is ext-real real V65() Element of REAL
r + (r + n) is ext-real real V65() set
(r + (r + n)) / 2 is ext-real real V65() Element of REAL
n is ext-real real V65() set
[#] REAL is non empty non proper complex-membered ext-real-membered real-membered closed open Element of K32(REAL)
r is complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval Element of K32(REAL)
lower_bound r is ext-real real V65() Element of REAL
upper_bound r is ext-real real V65() Element of REAL
[.(lower_bound r),(upper_bound r).] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
s is non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval Element of K32(REAL)
lower_bound s is ext-real real V65() Element of REAL
inf s is ext-real real V65() set
upper_bound s is ext-real real V65() Element of REAL
sup s is ext-real real V65() set
[.(lower_bound s),(upper_bound s).] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
r is complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded Element of K32(REAL)
lower_bound r is ext-real real V65() Element of REAL
upper_bound r is ext-real real V65() Element of REAL
].(lower_bound r),(upper_bound r).] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
s is set
n is ext-real real V65() Element of REAL
r is complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval Element of K32(REAL)
lower_bound r is ext-real real V65() Element of REAL
upper_bound r is ext-real real V65() Element of REAL
].(lower_bound r),(upper_bound r).] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
s is set
n is ext-real real V65() Element of REAL
n - (lower_bound r) is ext-real real V65() Element of REAL
(lower_bound r) - (lower_bound r) is ext-real real V65() Element of REAL
(lower_bound r) + (n - (lower_bound r)) is ext-real real V65() Element of REAL
F is ext-real real V65() set
[.F,(upper_bound r).] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
r is complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded Element of K32(REAL)
upper_bound r is ext-real real V65() Element of REAL
lower_bound r is ext-real real V65() Element of REAL
[.(lower_bound r),(upper_bound r).[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
s is set
n is ext-real real V65() Element of REAL
r is complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval Element of K32(REAL)
lower_bound r is ext-real real V65() Element of REAL
upper_bound r is ext-real real V65() Element of REAL
[.(lower_bound r),(upper_bound r).[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
s is set
n is ext-real real V65() Element of REAL
(upper_bound r) - n is ext-real real V65() Element of REAL
n - n is ext-real real V65() Element of REAL
(upper_bound r) - ((upper_bound r) - n) is ext-real real V65() Element of REAL
F is ext-real real V65() set
[.(lower_bound r),F.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
r is complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded Element of K32(REAL)
lower_bound r is ext-real real V65() Element of REAL
upper_bound r is ext-real real V65() Element of REAL
].(lower_bound r),(upper_bound r).[ is complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
s is set
n is ext-real real V65() Element of REAL
r is non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval Element of K32(REAL)
lower_bound r is ext-real real V65() Element of REAL
inf r is ext-real real V65() set
upper_bound r is ext-real real V65() Element of REAL
sup r is ext-real real V65() set
].(lower_bound r),(upper_bound r).[ is complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
s is set
n is ext-real real V65() Element of REAL
n - (lower_bound r) is ext-real real V65() Element of REAL
(lower_bound r) - (lower_bound r) is ext-real real V65() Element of REAL
(lower_bound r) + (n - (lower_bound r)) is ext-real real V65() Element of REAL
F is ext-real real V65() set
(upper_bound r) - n is ext-real real V65() Element of REAL
n - n is ext-real real V65() Element of REAL
(upper_bound r) - ((upper_bound r) - n) is ext-real real V65() Element of REAL
C is ext-real real V65() set
[.F,C.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
r is complex-membered ext-real-membered real-membered Element of K32(REAL)
upper_bound r is ext-real real V65() Element of REAL
left_closed_halfline (upper_bound r) is complex-membered ext-real-membered real-membered closed non bounded_below bounded_above interval Element of K32(REAL)
].-infty,(upper_bound r).] is complex-membered ext-real-membered real-membered non left_end bounded_above interval set
s is set
n is ext-real real V65() Element of REAL
r is complex-membered ext-real-membered real-membered interval Element of K32(REAL)
upper_bound r is ext-real real V65() Element of REAL
left_closed_halfline (upper_bound r) is complex-membered ext-real-membered real-membered closed non bounded_below bounded_above interval Element of K32(REAL)
].-infty,(upper_bound r).] is complex-membered ext-real-membered real-membered non left_end bounded_above interval set
s is set
n is ext-real real V65() Element of REAL
F is ext-real set
C is ext-real real V65() set
[.C,(upper_bound r).] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
r is complex-membered ext-real-membered real-membered Element of K32(REAL)
upper_bound r is ext-real real V65() Element of REAL
left_open_halfline (upper_bound r) is complex-membered ext-real-membered real-membered open non bounded_below bounded_above interval Element of K32(REAL)
].-infty,(upper_bound r).[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set
s is set
n is ext-real real V65() Element of REAL
r is non empty complex-membered ext-real-membered real-membered interval Element of K32(REAL)
upper_bound r is ext-real real V65() Element of REAL
left_open_halfline (upper_bound r) is complex-membered ext-real-membered real-membered open non bounded_below bounded_above interval Element of K32(REAL)
].-infty,(upper_bound r).[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set
s is set
n is ext-real real V65() Element of REAL
F is ext-real set
(upper_bound r) - n is ext-real real V65() Element of REAL
n - n is ext-real real V65() Element of REAL
(upper_bound r) - ((upper_bound r) - n) is ext-real real V65() Element of REAL
G is ext-real real V65() set
C is ext-real real V65() set
[.C,G.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
r is complex-membered ext-real-membered real-membered Element of K32(REAL)
lower_bound r is ext-real real V65() Element of REAL
right_closed_halfline (lower_bound r) is complex-membered ext-real-membered real-membered closed bounded_below non bounded_above interval Element of K32(REAL)
[.(lower_bound r),+infty.[ is complex-membered ext-real-membered real-membered non right_end bounded_below interval set
s is set
n is ext-real real V65() Element of REAL
r is complex-membered ext-real-membered real-membered interval Element of K32(REAL)
lower_bound r is ext-real real V65() Element of REAL
right_closed_halfline (lower_bound r) is complex-membered ext-real-membered real-membered closed bounded_below non bounded_above interval Element of K32(REAL)
[.(lower_bound r),+infty.[ is complex-membered ext-real-membered real-membered non right_end bounded_below interval set
s is set
n is ext-real real V65() Element of REAL
F is ext-real set
C is ext-real real V65() set
[.(lower_bound r),C.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
r is complex-membered ext-real-membered real-membered Element of K32(REAL)
lower_bound r is ext-real real V65() Element of REAL
right_open_halfline (lower_bound r) is complex-membered ext-real-membered real-membered open bounded_below non bounded_above interval Element of K32(REAL)
].(lower_bound r),+infty.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set
s is set
n is ext-real real V65() Element of REAL
r is non empty complex-membered ext-real-membered real-membered interval Element of K32(REAL)
lower_bound r is ext-real real V65() Element of REAL
right_open_halfline (lower_bound r) is complex-membered ext-real-membered real-membered open bounded_below non bounded_above interval Element of K32(REAL)
].(lower_bound r),+infty.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set
s is set
n is ext-real real V65() Element of REAL
F is ext-real set
n - (lower_bound r) is ext-real real V65() Element of REAL
(lower_bound r) - (lower_bound r) is ext-real real V65() Element of REAL
(lower_bound r) + (n - (lower_bound r)) is ext-real real V65() Element of REAL
C is ext-real real V65() set
G is ext-real real V65() set
[.C,G.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
r is complex-membered ext-real-membered real-membered interval Element of K32(REAL)
s is set
n is ext-real real V65() Element of REAL
F is ext-real set
G is ext-real set
L is ext-real real V65() set
C is ext-real real V65() set
[.L,C.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
r is complex-membered ext-real-membered real-membered interval Element of K32(REAL)
s is non empty complex-membered ext-real-membered real-membered interval Element of K32(REAL)
n is non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval Element of K32(REAL)
F is set
{F} is non empty trivial finite 1 -element set
C is ext-real real V65() Element of REAL
[.C,C.] is non empty complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
n is non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval Element of K32(REAL)
upper_bound n is ext-real real V65() Element of REAL
sup n is ext-real real V65() set
lower_bound n is ext-real real V65() Element of REAL
inf n is ext-real real V65() set
F is set
C is set
[.(lower_bound n),(upper_bound n).] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
].(lower_bound n),(upper_bound n).] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
[.(lower_bound n),(upper_bound n).[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
].(lower_bound n),(upper_bound n).[ is complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
n is non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval Element of K32(REAL)
s is non empty complex-membered ext-real-membered real-membered interval Element of K32(REAL)
upper_bound s is ext-real real V65() Element of REAL
left_closed_halfline (upper_bound s) is complex-membered ext-real-membered real-membered closed non bounded_below bounded_above interval Element of K32(REAL)
].-infty,(upper_bound s).] is complex-membered ext-real-membered real-membered non left_end bounded_above interval set
upper_bound s is ext-real real V65() Element of REAL
left_open_halfline (upper_bound s) is complex-membered ext-real-membered real-membered open non bounded_below bounded_above interval Element of K32(REAL)
].-infty,(upper_bound s).[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set
upper_bound s is ext-real real V65() Element of REAL
lower_bound s is ext-real real V65() Element of REAL
right_closed_halfline (lower_bound s) is complex-membered ext-real-membered real-membered closed bounded_below non bounded_above interval Element of K32(REAL)
[.(lower_bound s),+infty.[ is complex-membered ext-real-membered real-membered non right_end bounded_below interval set
lower_bound s is ext-real real V65() Element of REAL
right_open_halfline (lower_bound s) is complex-membered ext-real-membered real-membered open bounded_below non bounded_above interval Element of K32(REAL)
].(lower_bound s),+infty.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set
lower_bound s is ext-real real V65() Element of REAL
s is non empty complex-membered ext-real-membered real-membered interval Element of K32(REAL)
r is ext-real real V65() set
s is non empty complex-membered ext-real-membered real-membered interval Element of K32(REAL)
lower_bound s is ext-real real V65() Element of REAL
upper_bound s is ext-real real V65() Element of REAL
n is ext-real real V65() set
left_closed_halfline n is complex-membered ext-real-membered real-membered closed non bounded_below bounded_above interval Element of K32(REAL)
].-infty,n.] is complex-membered ext-real-membered real-membered non left_end bounded_above interval set
n is ext-real real V65() set
left_closed_halfline n is complex-membered ext-real-membered real-membered closed non bounded_below bounded_above interval Element of K32(REAL)
].-infty,n.] is complex-membered ext-real-membered real-membered non left_end bounded_above interval set
n is ext-real real V65() set
left_open_halfline n is complex-membered ext-real-membered real-membered open non bounded_below bounded_above interval Element of K32(REAL)
].-infty,n.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set
n is ext-real real V65() set
left_open_halfline n is complex-membered ext-real-membered real-membered open non bounded_below bounded_above interval Element of K32(REAL)
].-infty,n.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set
n is ext-real real V65() set
right_closed_halfline n is complex-membered ext-real-membered real-membered closed bounded_below non bounded_above interval Element of K32(REAL)
[.n,+infty.[ is complex-membered ext-real-membered real-membered non right_end bounded_below interval set
n is ext-real real V65() set
right_closed_halfline n is complex-membered ext-real-membered real-membered closed bounded_below non bounded_above interval Element of K32(REAL)
[.n,+infty.[ is complex-membered ext-real-membered real-membered non right_end bounded_below interval set
n is ext-real real V65() set
right_open_halfline n is complex-membered ext-real-membered real-membered open bounded_below non bounded_above interval Element of K32(REAL)
].n,+infty.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set
n is ext-real real V65() set
right_open_halfline n is complex-membered ext-real-membered real-membered open bounded_below non bounded_above interval Element of K32(REAL)
].n,+infty.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set
n is ext-real real V65() set
F is ext-real real V65() set
[.n,F.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
n is ext-real real V65() set
F is ext-real real V65() set
[.n,F.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
F is ext-real real V65() set
n is ext-real real V65() set
[.n,F.[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
F is ext-real real V65() set
n is ext-real real V65() set
[.n,F.[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
F is ext-real real V65() set
n is ext-real real V65() set
].n,F.] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
F is ext-real real V65() set
n is ext-real real V65() set
].n,F.] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
F is ext-real real V65() set
n is ext-real real V65() set
].n,F.[ is complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
F is ext-real real V65() set
n is ext-real real V65() set
].n,F.[ is complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
r is non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval Element of K32(REAL)
lower_bound r is ext-real real V65() Element of REAL
inf r is ext-real real V65() set
s is non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval Element of K32(REAL)
lower_bound s is ext-real real V65() Element of REAL
inf s is ext-real real V65() set
upper_bound s is ext-real real V65() Element of REAL
sup s is ext-real real V65() set
upper_bound r is ext-real real V65() Element of REAL
sup r is ext-real real V65() set
n is set
[.(lower_bound s),(upper_bound s).] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
F is ext-real real V65() Element of REAL
C is ext-real real V65() set
left_closed_halfline C is complex-membered ext-real-membered real-membered closed non bounded_below bounded_above interval Element of K32(REAL)
].-infty,C.] is complex-membered ext-real-membered real-membered non left_end bounded_above interval set
G is ext-real real V65() set
left_open_halfline G is complex-membered ext-real-membered real-membered open non bounded_below bounded_above interval Element of K32(REAL)
].-infty,G.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set
L is ext-real real V65() set
right_closed_halfline L is complex-membered ext-real-membered real-membered closed bounded_below non bounded_above interval Element of K32(REAL)
[.L,+infty.[ is complex-membered ext-real-membered real-membered non right_end bounded_below interval set
k is ext-real real V65() set
right_open_halfline k is complex-membered ext-real-membered real-membered open bounded_below non bounded_above interval Element of K32(REAL)
].k,+infty.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set
C is ext-real real V65() set
G is ext-real real V65() set
[.C,G.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
C is ext-real real V65() set
G is ext-real real V65() set
[.C,G.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
G is ext-real real V65() set
C is ext-real real V65() set
[.C,G.[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
G is ext-real real V65() set
C is ext-real real V65() set
[.C,G.[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
L is ext-real real V65() set
left_closed_halfline L is complex-membered ext-real-membered real-membered closed non bounded_below bounded_above interval Element of K32(REAL)
].-infty,L.] is complex-membered ext-real-membered real-membered non left_end bounded_above interval set
k is ext-real real V65() set
left_open_halfline k is complex-membered ext-real-membered real-membered open non bounded_below bounded_above interval Element of K32(REAL)
].-infty,k.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set
z is ext-real real V65() set
right_closed_halfline z is complex-membered ext-real-membered real-membered closed bounded_below non bounded_above interval Element of K32(REAL)
[.z,+infty.[ is complex-membered ext-real-membered real-membered non right_end bounded_below interval set
x is ext-real real V65() set
right_open_halfline x is complex-membered ext-real-membered real-membered open bounded_below non bounded_above interval Element of K32(REAL)
].x,+infty.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set
L is ext-real real V65() set
k is ext-real real V65() set
[.L,k.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
L is ext-real real V65() set
k is ext-real real V65() set
[.L,k.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
k is ext-real real V65() set
L is ext-real real V65() set
[.L,k.[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
k is ext-real real V65() set
L is ext-real real V65() set
[.L,k.[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
k is ext-real real V65() set
L is ext-real real V65() set
].L,k.] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
k is ext-real real V65() set
L is ext-real real V65() set
].L,k.] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
k is ext-real real V65() set
L is ext-real real V65() set
].L,k.[ is complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
k is ext-real real V65() set
L is ext-real real V65() set
].L,k.[ is complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
G is ext-real real V65() set
C is ext-real real V65() set
].C,G.] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
G is ext-real real V65() set
C is ext-real real V65() set
].C,G.] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
L is ext-real real V65() set
left_closed_halfline L is complex-membered ext-real-membered real-membered closed non bounded_below bounded_above interval Element of K32(REAL)
].-infty,L.] is complex-membered ext-real-membered real-membered non left_end bounded_above interval set
k is ext-real real V65() set
left_open_halfline k is complex-membered ext-real-membered real-membered open non bounded_below bounded_above interval Element of K32(REAL)
].-infty,k.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set
z is ext-real real V65() set
right_closed_halfline z is complex-membered ext-real-membered real-membered closed bounded_below non bounded_above interval Element of K32(REAL)
[.z,+infty.[ is complex-membered ext-real-membered real-membered non right_end bounded_below interval set
x is ext-real real V65() set
right_open_halfline x is complex-membered ext-real-membered real-membered open bounded_below non bounded_above interval Element of K32(REAL)
].x,+infty.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set
L is ext-real real V65() set
k is ext-real real V65() set
[.L,k.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
L is ext-real real V65() set
k is ext-real real V65() set
[.L,k.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
k is ext-real real V65() set
L is ext-real real V65() set
[.L,k.[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
k is ext-real real V65() set
L is ext-real real V65() set
[.L,k.[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
k is ext-real real V65() set
L is ext-real real V65() set
].L,k.] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
k is ext-real real V65() set
L is ext-real real V65() set
].L,k.] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
k is ext-real real V65() set
L is ext-real real V65() set
].L,k.[ is complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
k is ext-real real V65() set
L is ext-real real V65() set
].L,k.[ is complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
G is ext-real real V65() set
C is ext-real real V65() set
].C,G.[ is complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
G is ext-real real V65() set
C is ext-real real V65() set
].C,G.[ is complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
L is ext-real real V65() set
left_closed_halfline L is complex-membered ext-real-membered real-membered closed non bounded_below bounded_above interval Element of K32(REAL)
].-infty,L.] is complex-membered ext-real-membered real-membered non left_end bounded_above interval set
k is ext-real real V65() set
left_open_halfline k is complex-membered ext-real-membered real-membered open non bounded_below bounded_above interval Element of K32(REAL)
].-infty,k.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set
z is ext-real real V65() set
right_closed_halfline z is complex-membered ext-real-membered real-membered closed bounded_below non bounded_above interval Element of K32(REAL)
[.z,+infty.[ is complex-membered ext-real-membered real-membered non right_end bounded_below interval set
x is ext-real real V65() set
right_open_halfline x is complex-membered ext-real-membered real-membered open bounded_below non bounded_above interval Element of K32(REAL)
].x,+infty.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set
L is ext-real real V65() set
k is ext-real real V65() set
[.L,k.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
L is ext-real real V65() set
k is ext-real real V65() set
[.L,k.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
k is ext-real real V65() set
L is ext-real real V65() set
[.L,k.[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
k is ext-real real V65() set
L is ext-real real V65() set
[.L,k.[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
k is ext-real real V65() set
L is ext-real real V65() set
].L,k.] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
k is ext-real real V65() set
L is ext-real real V65() set
].L,k.] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
k is ext-real real V65() set
L is ext-real real V65() set
].L,k.[ is complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
k is ext-real real V65() set
L is ext-real real V65() set
].L,k.[ is complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
r is ext-real real V65() set
s is ext-real real V65() set
[.r,s.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
{r,s} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
n is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
Fr n is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
Cl n is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
Cl [.r,s.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded Element of K32(REAL)
left_closed_halfline r is complex-membered ext-real-membered real-membered closed non bounded_below bounded_above interval Element of K32(REAL)
].-infty,r.] is complex-membered ext-real-membered real-membered non left_end bounded_above interval set
right_closed_halfline s is complex-membered ext-real-membered real-membered closed bounded_below non bounded_above interval Element of K32(REAL)
[.s,+infty.[ is complex-membered ext-real-membered real-membered non right_end bounded_below interval set
(left_closed_halfline r) \/ (right_closed_halfline s) is complex-membered ext-real-membered real-membered Element of K32(REAL)
[.r,s.] /\ ((left_closed_halfline r) \/ (right_closed_halfline s)) is complex-membered ext-real-membered real-membered Element of K32(REAL)
left_open_halfline r is complex-membered ext-real-membered real-membered open non bounded_below bounded_above interval Element of K32(REAL)
].-infty,r.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set
R^1 (left_open_halfline r) is open complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
R^1 (right_closed_halfline s) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
right_open_halfline s is complex-membered ext-real-membered real-membered open bounded_below non bounded_above interval Element of K32(REAL)
].s,+infty.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set
R^1 (right_open_halfline s) is open complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
R^1 (left_closed_halfline r) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
[.r,s.] ` is complex-membered ext-real-membered real-membered Element of K32(REAL)
REAL \ [.r,s.] is complex-membered ext-real-membered real-membered set
(R^1 (left_open_halfline r)) \/ (R^1 (right_open_halfline s)) is open complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
n ` is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
the carrier of R^1 \ n is complex-membered ext-real-membered real-membered set
Cl (n `) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
Cl ([.r,s.] `) is complex-membered ext-real-membered real-membered closed Element of K32(REAL)
Cl (left_open_halfline r) is complex-membered ext-real-membered real-membered closed bounded_above Element of K32(REAL)
Cl (right_open_halfline s) is complex-membered ext-real-membered real-membered closed bounded_below Element of K32(REAL)
(Cl (left_open_halfline r)) \/ (Cl (right_open_halfline s)) is complex-membered ext-real-membered real-membered Element of K32(REAL)
Cl (R^1 (left_open_halfline r)) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
(Cl (R^1 (left_open_halfline r))) \/ (Cl (right_open_halfline s)) is complex-membered ext-real-membered real-membered set
Cl (R^1 (right_open_halfline s)) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
(Cl (R^1 (left_open_halfline r))) \/ (Cl (R^1 (right_open_halfline s))) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
(R^1 (left_closed_halfline r)) \/ (Cl (R^1 (right_open_halfline s))) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
(R^1 (left_closed_halfline r)) \/ (R^1 (right_closed_halfline s)) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
r is ext-real real V65() set
s is ext-real real V65() set
].r,s.[ is complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
{r,s} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
n is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
Fr n is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
Cl n is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
Cl ].r,s.[ is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded Element of K32(REAL)
[.r,s.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
right_closed_halfline s is complex-membered ext-real-membered real-membered closed bounded_below non bounded_above interval Element of K32(REAL)
[.s,+infty.[ is complex-membered ext-real-membered real-membered non right_end bounded_below interval set
R^1 (right_closed_halfline s) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
left_closed_halfline r is complex-membered ext-real-membered real-membered closed non bounded_below bounded_above interval Element of K32(REAL)
].-infty,r.] is complex-membered ext-real-membered real-membered non left_end bounded_above interval set
R^1 (left_closed_halfline r) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
].r,s.[ ` is complex-membered ext-real-membered real-membered Element of K32(REAL)
REAL \ ].r,s.[ is complex-membered ext-real-membered real-membered set
(R^1 (left_closed_halfline r)) \/ (R^1 (right_closed_halfline s)) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
(left_closed_halfline r) \/ (right_closed_halfline s) is complex-membered ext-real-membered real-membered Element of K32(REAL)
[.r,s.] /\ ((left_closed_halfline r) \/ (right_closed_halfline s)) is complex-membered ext-real-membered real-membered Element of K32(REAL)
n ` is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
the carrier of R^1 \ n is complex-membered ext-real-membered real-membered set
Cl (n `) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
Cl (].r,s.[ `) is complex-membered ext-real-membered real-membered closed Element of K32(REAL)
Cl (left_closed_halfline r) is complex-membered ext-real-membered real-membered closed bounded_above Element of K32(REAL)
Cl (right_closed_halfline s) is complex-membered ext-real-membered real-membered closed bounded_below Element of K32(REAL)
(Cl (left_closed_halfline r)) \/ (Cl (right_closed_halfline s)) is complex-membered ext-real-membered real-membered Element of K32(REAL)
(Cl (left_closed_halfline r)) \/ (right_closed_halfline s) is complex-membered ext-real-membered real-membered Element of K32(REAL)
r is ext-real real V65() set
s is ext-real real V65() set
[.r,s.[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
{r,s} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
n is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
Fr n is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
Cl n is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
[.r,s.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
left_closed_halfline r is complex-membered ext-real-membered real-membered closed non bounded_below bounded_above interval Element of K32(REAL)
].-infty,r.] is complex-membered ext-real-membered real-membered non left_end bounded_above interval set
right_closed_halfline s is complex-membered ext-real-membered real-membered closed bounded_below non bounded_above interval Element of K32(REAL)
[.s,+infty.[ is complex-membered ext-real-membered real-membered non right_end bounded_below interval set
(left_closed_halfline r) \/ (right_closed_halfline s) is complex-membered ext-real-membered real-membered Element of K32(REAL)
[.r,s.] /\ ((left_closed_halfline r) \/ (right_closed_halfline s)) is complex-membered ext-real-membered real-membered Element of K32(REAL)
left_open_halfline r is complex-membered ext-real-membered real-membered open non bounded_below bounded_above interval Element of K32(REAL)
].-infty,r.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set
R^1 (left_open_halfline r) is open complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
R^1 (right_closed_halfline s) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
R^1 (left_closed_halfline r) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
[.r,s.[ ` is complex-membered ext-real-membered real-membered Element of K32(REAL)
REAL \ [.r,s.[ is complex-membered ext-real-membered real-membered set
(R^1 (left_open_halfline r)) \/ (R^1 (right_closed_halfline s)) is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
n ` is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
the carrier of R^1 \ n is complex-membered ext-real-membered real-membered set
Cl (n `) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
Cl ([.r,s.[ `) is complex-membered ext-real-membered real-membered closed Element of K32(REAL)
Cl (left_open_halfline r) is complex-membered ext-real-membered real-membered closed bounded_above Element of K32(REAL)
Cl (right_closed_halfline s) is complex-membered ext-real-membered real-membered closed bounded_below Element of K32(REAL)
(Cl (left_open_halfline r)) \/ (Cl (right_closed_halfline s)) is complex-membered ext-real-membered real-membered Element of K32(REAL)
Cl (R^1 (left_open_halfline r)) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
(Cl (R^1 (left_open_halfline r))) \/ (Cl (right_closed_halfline s)) is complex-membered ext-real-membered real-membered set
Cl (R^1 (right_closed_halfline s)) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
(Cl (R^1 (left_open_halfline r))) \/ (Cl (R^1 (right_closed_halfline s))) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
(R^1 (left_closed_halfline r)) \/ (Cl (R^1 (right_closed_halfline s))) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
r is ext-real real V65() set
s is ext-real real V65() set
].r,s.] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
{r,s} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
n is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
Fr n is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
Cl n is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
[.r,s.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
left_closed_halfline r is complex-membered ext-real-membered real-membered closed non bounded_below bounded_above interval Element of K32(REAL)
].-infty,r.] is complex-membered ext-real-membered real-membered non left_end bounded_above interval set
right_closed_halfline s is complex-membered ext-real-membered real-membered closed bounded_below non bounded_above interval Element of K32(REAL)
[.s,+infty.[ is complex-membered ext-real-membered real-membered non right_end bounded_below interval set
(left_closed_halfline r) \/ (right_closed_halfline s) is complex-membered ext-real-membered real-membered Element of K32(REAL)
[.r,s.] /\ ((left_closed_halfline r) \/ (right_closed_halfline s)) is complex-membered ext-real-membered real-membered Element of K32(REAL)
].r,s.] ` is complex-membered ext-real-membered real-membered Element of K32(REAL)
REAL \ ].r,s.] is complex-membered ext-real-membered real-membered set
right_open_halfline s is complex-membered ext-real-membered real-membered open bounded_below non bounded_above interval Element of K32(REAL)
].s,+infty.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set
(left_closed_halfline r) \/ (right_open_halfline s) is complex-membered ext-real-membered real-membered Element of K32(REAL)
R^1 (right_open_halfline s) is open complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
R^1 (left_closed_halfline r) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
n ` is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
the carrier of R^1 \ n is complex-membered ext-real-membered real-membered set
Cl (n `) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
Cl (].r,s.] `) is complex-membered ext-real-membered real-membered closed Element of K32(REAL)
Cl (left_closed_halfline r) is complex-membered ext-real-membered real-membered closed bounded_above Element of K32(REAL)
Cl (right_open_halfline s) is complex-membered ext-real-membered real-membered closed bounded_below Element of K32(REAL)
(Cl (left_closed_halfline r)) \/ (Cl (right_open_halfline s)) is complex-membered ext-real-membered real-membered Element of K32(REAL)
Cl (R^1 (left_closed_halfline r)) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
(Cl (R^1 (left_closed_halfline r))) \/ (Cl (right_open_halfline s)) is complex-membered ext-real-membered real-membered set
Cl (R^1 (right_open_halfline s)) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
(Cl (R^1 (left_closed_halfline r))) \/ (Cl (R^1 (right_open_halfline s))) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
(R^1 (left_closed_halfline r)) \/ (Cl (R^1 (right_open_halfline s))) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
r is ext-real real V65() set
s is ext-real real V65() set
[.r,s.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
].r,s.[ is complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
n is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
Int n is open complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
F is set
{} R^1 is Relation-like non-empty empty-yielding RAT -valued functional ordinal natural empty proper ext-real non positive non negative finite finite-yielding V43() cardinal {} -element real V65() V66() FinSequence-like FinSequence-membered open closed boundary nowhere_dense connected complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() V124() V125() V126() V127() bounded_below bounded_above real-bounded interval Element of K32( the carrier of R^1)
Fr n is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
{r,s} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
C is ext-real real V65() Element of the carrier of R^1
F is open complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
r is ext-real real V65() set
s is ext-real real V65() set
].r,s.[ is complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
n is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
Int n is open complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
F is open complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
Int F is open complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
r is ext-real real V65() set
s is ext-real real V65() set
[.r,s.[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
].r,s.[ is complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
n is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
Int n is open complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
F is set
{} R^1 is Relation-like non-empty empty-yielding RAT -valued functional ordinal natural empty proper ext-real non positive non negative finite finite-yielding V43() cardinal {} -element real V65() V66() FinSequence-like FinSequence-membered open closed boundary nowhere_dense connected complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() V124() V125() V126() V127() bounded_below bounded_above real-bounded interval Element of K32( the carrier of R^1)
Fr n is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
{r,s} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
C is ext-real real V65() Element of the carrier of R^1
F is open complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
r is ext-real real V65() set
s is ext-real real V65() set
].r,s.] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
].r,s.[ is complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
n is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
Int n is open complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
F is set
{} R^1 is Relation-like non-empty empty-yielding RAT -valued functional ordinal natural empty proper ext-real non positive non negative finite finite-yielding V43() cardinal {} -element real V65() V66() FinSequence-like FinSequence-membered open closed boundary nowhere_dense connected complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() V124() V125() V126() V127() bounded_below bounded_above real-bounded interval Element of K32( the carrier of R^1)
Fr n is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
{r,s} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
C is ext-real real V65() Element of the carrier of R^1
F is open complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
r is real-membered TopStruct
the carrier of r is complex-membered ext-real-membered real-membered set
K32( the carrier of r) is non empty set
s is complex-membered ext-real-membered real-membered interval Element of K32( the carrier of r)
r | s is strict real-membered SubSpace of r
[#] (r | s) is non proper dense complex-membered ext-real-membered real-membered Element of K32( the carrier of (r | s))
the carrier of (r | s) is complex-membered ext-real-membered real-membered set
K32( the carrier of (r | s)) is non empty set
r is complex-membered ext-real-membered real-membered interval Element of K32(REAL)
R^1 r is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
r is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
s is ext-real set
n is ext-real set
[.s,n.] is ext-real-membered interval set
r is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
s is Relation-like non-empty empty-yielding RAT -valued functional ordinal natural empty proper ext-real non positive non negative finite finite-yielding V43() cardinal {} -element real V65() V66() FinSequence-like FinSequence-membered open closed boundary nowhere_dense connected complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() V124() V125() V126()