:: RCOMP_3 semantic presentation

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() V127() bounded_below bounded_above real-bounded interval Element of K32( the carrier of R^1)
s is non empty complex-membered ext-real-membered real-membered interval Element of K32( the carrier of R^1)
R^1 | s is non empty strict TopSpace-like connected real-membered interval V241() SubSpace of R^1
R^1 | r is strict TopSpace-like real-membered SubSpace of R^1
s is ext-real real V65() set
left_closed_halfline s is complex-membered ext-real-membered real-membered closed non bounded_below bounded_above interval Element of K32(REAL)
].-infty,s.] is complex-membered ext-real-membered real-membered non left_end bounded_above interval set
s is ext-real real V65() set
left_closed_halfline s is complex-membered ext-real-membered real-membered closed non bounded_below bounded_above interval Element of K32(REAL)
].-infty,s.] is complex-membered ext-real-membered real-membered non left_end bounded_above interval set
n is non empty complex-membered ext-real-membered real-membered interval Element of K32( the carrier of R^1)
R^1 | n is non empty strict TopSpace-like connected real-membered interval V241() SubSpace of R^1
R^1 | r is strict TopSpace-like real-membered SubSpace of R^1
s is ext-real real V65() set
left_open_halfline s is complex-membered ext-real-membered real-membered open non bounded_below bounded_above interval Element of K32(REAL)
].-infty,s.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set
s is ext-real real V65() set
left_open_halfline s is complex-membered ext-real-membered real-membered open non bounded_below bounded_above interval Element of K32(REAL)
].-infty,s.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set
n is non empty complex-membered ext-real-membered real-membered interval Element of K32( the carrier of R^1)
R^1 | n is non empty strict TopSpace-like connected real-membered interval V241() SubSpace of R^1
R^1 | r is strict TopSpace-like real-membered SubSpace of R^1
s is ext-real real V65() 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
s is ext-real real V65() 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
n is non empty complex-membered ext-real-membered real-membered interval Element of K32( the carrier of R^1)
R^1 | n is non empty strict TopSpace-like connected real-membered interval V241() SubSpace of R^1
R^1 | r is strict TopSpace-like real-membered SubSpace of R^1
s is ext-real real V65() 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
s is ext-real real V65() 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
n is non empty complex-membered ext-real-membered real-membered interval Element of K32( the carrier of R^1)
R^1 | n is non empty strict TopSpace-like connected real-membered interval V241() SubSpace of R^1
R^1 | r is strict TopSpace-like real-membered SubSpace of R^1
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)
s is non empty complex-membered ext-real-membered real-membered interval Element of K32( the carrier of R^1)
R^1 | s is non empty strict TopSpace-like connected real-membered interval V241() SubSpace of R^1
R^1 | r is strict TopSpace-like real-membered SubSpace of R^1
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)
s is non empty complex-membered ext-real-membered real-membered interval Element of K32( the carrier of R^1)
R^1 | s is non empty strict TopSpace-like connected real-membered interval V241() SubSpace of R^1
R^1 | r is strict TopSpace-like real-membered SubSpace of R^1
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)
s is non empty complex-membered ext-real-membered real-membered interval Element of K32( the carrier of R^1)
R^1 | s is non empty strict TopSpace-like connected real-membered interval V241() SubSpace of R^1
R^1 | r is strict TopSpace-like real-membered SubSpace of R^1
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)
s is non empty complex-membered ext-real-membered real-membered interval Element of K32( the carrier of R^1)
R^1 | s is non empty strict TopSpace-like connected real-membered interval V241() SubSpace of R^1
R^1 | r is strict TopSpace-like real-membered SubSpace of R^1
r is ext-real real V65() set
Closed-Interval-TSpace (r,r) is non empty strict TopSpace-like real-membered SubSpace of R^1
{r} is non empty trivial finite 1 -element complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded Element of K32(REAL)
the carrier of (Closed-Interval-TSpace (r,r)) is non empty complex-membered ext-real-membered real-membered set
[.r,r.] is non empty complex-membered ext-real-membered real-membered closed 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
Closed-Interval-TSpace (r,s) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (r,s)) is non empty complex-membered ext-real-membered real-membered set
K32( the carrier of (Closed-Interval-TSpace (r,s))) is non empty set
[.r,s.] is complex-membered ext-real-membered real-membered closed 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 (Closed-Interval-TSpace (r,s)))
r is ext-real real V65() set
s is ext-real real V65() set
Closed-Interval-TSpace (r,s) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (r,s)) is non empty complex-membered ext-real-membered real-membered set
K32( the carrier of (Closed-Interval-TSpace (r,s))) is non empty 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 non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
].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 + n is ext-real real V65() set
(r + n) / 2 is ext-real real V65() Element of REAL
].((r + n) / 2),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^1 ].((r + n) / 2),F.[ is open connected complex-membered ext-real-membered real-membered interval 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)
k is complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s)))
Int k is open complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s)))
z is set
x is ext-real real V65() Element of REAL
z is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
x is set
c₁₁ is ext-real real V65() Element of REAL
Int z 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
Closed-Interval-TSpace (r,s) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (r,s)) is non empty complex-membered ext-real-membered real-membered set
K32( the carrier of (Closed-Interval-TSpace (r,s))) is non empty 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 non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
].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 + s is ext-real real V65() set
(F + s) / 2 is ext-real real V65() Element of REAL
].n,((F + s) / 2).[ 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^1 ].n,((F + s) / 2).[ is open connected complex-membered ext-real-membered real-membered interval 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)
k is complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s)))
Int k is open complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s)))
z is set
x is ext-real real V65() Element of REAL
z is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
x is set
c₁₁ is ext-real real V65() Element of REAL
Int z 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
Closed-Interval-TSpace (r,s) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (r,s)) is non empty complex-membered ext-real-membered real-membered set
K32( the carrier of (Closed-Interval-TSpace (r,s))) is non empty set
n is complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s)))
F is complex-membered ext-real-membered real-membered Element of K32(REAL)
C is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)
r is TopSpace-like TopStruct
the carrier of r is set
K32( the carrier of r) is non empty set
{} r 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 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)
r is non empty TopSpace-like connected TopStruct
the carrier of r is non empty set
K32( the carrier of r) is non empty set
[#] r is non empty non proper open closed dense non boundary Element of K32( the carrier of r)
r is ext-real real V65() set
s is ext-real real V65() set
Closed-Interval-TSpace (r,s) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (r,s)) is non empty complex-membered ext-real-membered real-membered set
K32( the carrier of (Closed-Interval-TSpace (r,s))) is non empty set
[.r,s.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
F is open connected complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s)))
[#] (Closed-Interval-TSpace (r,s)) is non empty non proper open closed dense non boundary complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s)))
C is complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval Element of K32(REAL)
C is complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval Element of K32(REAL)
G is ext-real real V65() set
left_closed_halfline G is complex-membered ext-real-membered real-membered closed non bounded_below bounded_above interval Element of K32(REAL)
].-infty,G.] is complex-membered ext-real-membered real-membered non left_end bounded_above interval set
L is ext-real real V65() set
left_open_halfline L is complex-membered ext-real-membered real-membered open non bounded_below bounded_above interval Element of K32(REAL)
].-infty,L.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set
k is ext-real real V65() set
right_closed_halfline k is complex-membered ext-real-membered real-membered closed bounded_below non bounded_above interval Element of K32(REAL)
[.k,+infty.[ is complex-membered ext-real-membered real-membered non right_end bounded_below interval set
z is ext-real real V65() set
right_open_halfline z is complex-membered ext-real-membered real-membered open bounded_below non bounded_above interval Element of K32(REAL)
].z,+infty.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set
C is complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval Element of K32(REAL)
G is ext-real real V65() set
L is ext-real real V65() set
[.G,L.] 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
L is ext-real real V65() set
[.G,L.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
{} (Closed-Interval-TSpace (r,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() V127() bounded_below bounded_above real-bounded interval Element of K32( the carrier of (Closed-Interval-TSpace (r,s)))
C is complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval Element of K32(REAL)
L is ext-real real V65() set
G is ext-real real V65() set
[.G,L.[ 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
G is ext-real real V65() set
[.G,L.[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
Int F is open complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s)))
].G,L.[ 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)
C is complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval Element of K32(REAL)
L is ext-real real V65() set
G is ext-real real V65() set
].G,L.] 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
G is ext-real real V65() set
].G,L.] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
Int F is open complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s)))
].G,L.[ 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)
C is complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval Element of K32(REAL)
L is ext-real real V65() set
G is ext-real real V65() set
].G,L.[ 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
G is ext-real real V65() set
].G,L.[ 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)
C is complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval Element of K32(REAL)
r is 1-sorted
the carrier of r is set
K32( the carrier of r) is non empty set
K32(K32( the carrier of r)) is non empty set
s is finite Element of K32(K32( the carrier of r))
{ b₁ where b₁ is Element of K32( the carrier of r) : ( b₁ in s & ex b₂ being Element of K32( the carrier of r) st
( b₂ in s & b₁ c< b₂ ) ) } is set
s \ { b₁ where b₁ is Element of K32( the carrier of r) : ( b₁ in s & ex b₂ being Element of K32( the carrier of r) st
( b₂ in s & b₁ c< b₂ ) ) } is finite Element of K32(K32( the carrier of r))
n is Element of K32(K32( the carrier of r))
union s is Element of K32( the carrier of r)
union n is Element of K32( the carrier of r)
C is set
G is set
{ b₁ where b₁ is Element of K32( the carrier of r) : ( G c< b₁ & b₁ in s ) } is set
k is Element of K32( the carrier of r)
z is Element of K32( the carrier of r)
z is Element of K32( the carrier of r)
k is set
K33( { b₁ where b₁ is Element of K32( the carrier of r) : ( G c< b₁ & b₁ in s ) } , { b₁ where b₁ is Element of K32( the carrier of r) : ( G c< b₁ & b₁ in s ) } ) is Relation-like set
K32(K33( { b₁ where b₁ is Element of K32( the carrier of r) : ( G c< b₁ & b₁ in s ) } , { b₁ where b₁ is Element of K32( the carrier of r) : ( G c< b₁ & b₁ in s ) } )) is non empty set
z is Relation-like Element of K32(K33( { b₁ where b₁ is Element of K32( the carrier of r) : ( G c< b₁ & b₁ in s ) } , { b₁ where b₁ is Element of K32( the carrier of r) : ( G c< b₁ & b₁ in s ) } ))
x is set
[x,x] is set
{x,x} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,x},{x}} is non empty finite V43() set
field z is set
x is set
c₁₁ is set
T is set
[x,c₁₁] is set
{x,c₁₁} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,c₁₁},{x}} is non empty finite V43() set
[c₁₁,T] is set
{c₁₁,T} is non empty finite set
{c₁₁} is non empty trivial finite 1 -element set
{{c₁₁,T},{c₁₁}} is non empty finite V43() set
[x,T] is set
{x,T} is non empty finite set
{{x,T},{x}} is non empty finite V43() set
x is set
c₁₁ is set
[x,c₁₁] is set
{x,c₁₁} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,c₁₁},{x}} is non empty finite V43() set
[c₁₁,x] is set
{c₁₁,x} is non empty finite set
{c₁₁} is non empty trivial finite 1 -element set
{{c₁₁,x},{c₁₁}} is non empty finite V43() set
x is set
z |_2 x is Relation-like set
K33(x,x) is Relation-like set
z /\ K33(x,x) is Relation-like set
union x is set
field (z |_2 x) is set
c₁₁ is set
T is set
c₁₁ \/ T is set
[c₁₁,T] is set
{c₁₁,T} is non empty finite set
{c₁₁} is non empty trivial finite 1 -element set
{{c₁₁,T},{c₁₁}} is non empty finite V43() set
[T,c₁₁] is set
{T,c₁₁} is non empty finite set
{T} is non empty trivial finite 1 -element set
{{T,c₁₁},{T}} is non empty finite V43() set
c₁₁ is set
T is set
union T is set
{c₁₁} is non empty trivial finite 1 -element set
T \/ {c₁₁} is non empty set
union (T \/ {c₁₁}) is set
union {c₁₁} is set
c₁₁ \/ (union T) is set
c₁₁ is set
T is Element of K32( the carrier of r)
LM1 is set
RM1 is Element of K32( the carrier of r)
LM1 is set
[LM1,(union x)] is set
{LM1,(union x)} is non empty finite set
{LM1} is non empty trivial finite 1 -element set
{{LM1,(union x)},{LM1}} is non empty finite V43() set
c₁₁ is set
[c₁₁,k] is set
{c₁₁,k} is non empty finite set
{c₁₁} is non empty trivial finite 1 -element set
{{c₁₁,k},{c₁₁}} is non empty finite V43() set
x is set
c₁₁ is Element of K32( the carrier of r)
T is Element of K32( the carrier of r)
T is Element of K32( the carrier of r)
LM1 is Element of K32( the carrier of r)
[x,T] is set
{x,T} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,T},{x}} is non empty finite V43() set
c₁₁ is Element of K32( the carrier of r)
c₁₁ is Element of K32( the carrier of r)
r is non empty trivial finite 1 -element 1-sorted
the carrier of r is non empty trivial finite 1 -element set
K32( the carrier of r) is non empty finite V43() set
K32(K32( the carrier of r)) is non empty finite V43() set
s is Element of the carrier of r
{s} is non empty trivial finite 1 -element set
n is finite V43() Element of K32(K32( the carrier of r))
union n is trivial finite Element of K32( the carrier of r)
F is Element of the carrier of r
{F} is non empty trivial finite 1 -element set
C is set
G is set
G is set
r is TopStruct
the carrier of r is set
K32( the carrier of r) is non empty set
K32(K32( the carrier of r)) is non empty set
r is TopSpace-like TopStruct
the carrier of r is set
K32( the carrier of r) is non empty set
K32(K32( the carrier of r)) is non empty set
{} r 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 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)
{({} r)} 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 Element of K32(REAL)
bool the carrier of r is non empty Element of K32(K32( the carrier of r))
s is set
s is Element of K32(K32( the carrier of r))
n is Element of K32( the carrier of r)
n is Element of K32( the carrier of r)
n is Element of K32( the carrier of r)
r is ext-real real V65() set
s is ext-real real V65() set
Closed-Interval-TSpace (r,s) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (r,s)) is non empty complex-membered ext-real-membered real-membered set
K32( the carrier of (Closed-Interval-TSpace (r,s))) is non empty set
K32(K32( the carrier of (Closed-Interval-TSpace (r,s)))) is non empty 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 Relation-like NAT -defined K32(REAL) -valued Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of K32(REAL)
rng <*[.r,s.]*> is non empty trivial finite 1 -element Element of K32(K32(REAL))
union (rng <*[.r,s.]*>) is complex-membered ext-real-membered real-membered Element of K32(REAL)
len <*[.r,s.]*> 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
n is Element of K32(K32( the carrier of (Closed-Interval-TSpace (r,s))))
{[.r,s.]} is non empty trivial finite 1 -element set
C is set
C is ordinal natural ext-real non negative finite cardinal real V65() V66() set
<*[.r,s.]*> /. C is complex-membered ext-real-membered real-membered Element of K32(REAL)
C + 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
lower_bound (<*[.r,s.]*> /. C) is ext-real real V65() Element of REAL
<*[.r,s.]*> /. (C + 1) is complex-membered ext-real-membered real-membered Element of K32(REAL)
lower_bound (<*[.r,s.]*> /. (C + 1)) is ext-real real V65() Element of REAL
upper_bound (<*[.r,s.]*> /. C) is ext-real real V65() Element of REAL
upper_bound (<*[.r,s.]*> /. (C + 1)) is ext-real real V65() Element of REAL
C + 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
<*[.r,s.]*> /. (C + 2) is complex-membered ext-real-membered real-membered Element of K32(REAL)
lower_bound (<*[.r,s.]*> /. (C + 2)) is ext-real real V65() Element of REAL
0 + 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
(C + 1) + 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
r is TopSpace-like TopStruct
the carrier of r is set
K32( the carrier of r) is non empty set
K32(K32( the carrier of r)) is non empty set
s is Element of K32(K32( the carrier of r))
n is Element of K32(K32( the carrier of r))
{ b₁ where b₁ is Element of K32( the carrier of r) : ( b₁ in s & ex b₂ being Element of K32( the carrier of r) st
( b₂ in s & b₁ c< b₂ ) ) } is set
s \ { b₁ where b₁ is Element of K32( the carrier of r) : ( b₁ in s & ex b₂ being Element of K32( the carrier of r) st
( b₂ in s & b₁ c< b₂ ) ) } is Element of K32(K32( the carrier of r))
{ b₁ where b₁ is Element of K32(K32( the carrier of r)) : ( b₁ is Cover of the carrier of r & b₁ c= n ) } is set
F is set
RelIncl F is Relation-like reflexive antisymmetric transitive set
field (RelIncl F) is set
L is set
(RelIncl F) |_2 L is Relation-like set
K33(L,L) is Relation-like set
(RelIncl F) /\ K33(L,L) is Relation-like set
bool n is non empty Element of K32(K32(n))
K32(n) is non empty set
K32(K32(n)) is non empty set
{ H₁(b₁) where b₁ is Element of K32(K32( the carrier of r)) : b₁ in bool n } is set
meet L is set
z is set
x is set
c₁₁ is Element of K32(K32( the carrier of r))
x is set
c₁₁ is set
meet c₁₁ is set
{x} is non empty trivial finite 1 -element set
c₁₁ \/ {x} is non empty set
meet (c₁₁ \/ {x}) is set
field ((RelIncl F) |_2 L) is set
[x,(meet c₁₁)] is set
{x,(meet c₁₁)} is non empty finite set
{{x,(meet c₁₁)},{x}} is non empty finite V43() set
[(meet c₁₁),x] is set
{(meet c₁₁),x} is non empty finite set
{(meet c₁₁)} is non empty trivial finite 1 -element set
{{(meet c₁₁),x},{(meet c₁₁)}} is non empty finite V43() set
meet {x} is set
(meet c₁₁) /\ (meet {x}) is set
(meet c₁₁) /\ x is set
x is set
T is Element of K32(K32( the carrier of r))
meet {} is set
c₁₁ is Element of K32(K32( the carrier of r))
T is set
union c₁₁ is set
LM1 is Element of K32(K32( the carrier of r))
union LM1 is Element of K32( the carrier of r)
T is Element of K32(K32( the carrier of r))
T is set
[z,T] is set
{z,T} is non empty finite set
{z} is non empty trivial finite 1 -element set
{{z,T},{z}} is non empty finite V43() set
k is set
[n,k] is set
{n,k} is non empty finite set
{n} is non empty trivial finite 1 -element set
{{n,k},{n}} is non empty finite V43() set
r is TopSpace-like TopStruct
the carrier of r is set
K32( the carrier of r) is non empty set
K32(K32( the carrier of r)) is non empty set
s is set
{ b₁ where b₁ is Element of K32(K32( the carrier of r)) : ( b₁ is Cover of the carrier of r & b₁ c= s ) } is set
n is set
RelIncl n is Relation-like reflexive antisymmetric transitive set
field (RelIncl n) is set
C is set
G is Element of K32(K32( the carrier of r))
L is Element of K32( the carrier of r)
{L} is non empty trivial finite 1 -element set
G \ {L} is Element of K32(K32( the carrier of r))
z is Element of K32( the carrier of r)
x is Element of K32( the carrier of r)
z \/ x is Element of K32( the carrier of r)
union G is Element of K32( the carrier of r)
[#] r is non proper open closed dense Element of K32( the carrier of r)
union (G \ {L}) is Element of K32( the carrier of r)
c₁₁ is set
T is set
[(G \ {L}),C] is set
{(G \ {L}),C} is non empty finite set
{(G \ {L})} is non empty trivial finite 1 -element set
{{(G \ {L}),C},{(G \ {L})}} is non empty finite V43() set
r is ext-real real V65() set
s is ext-real real V65() set
Closed-Interval-TSpace (r,s) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (r,s)) is non empty complex-membered ext-real-membered real-membered set
K32( the carrier of (Closed-Interval-TSpace (r,s))) is non empty set
K32(K32( the carrier of (Closed-Interval-TSpace (r,s)))) is non empty set
n is Element of K32(K32( the carrier of (Closed-Interval-TSpace (r,s))))
bool REAL is non empty non trivial non finite Element of K32(K32(REAL))
[.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 Relation-like NAT -defined K32(REAL) -valued Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of K32(REAL)
F is Relation-like NAT -defined K32(REAL) -valued Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of K32(REAL)
rng F is non empty trivial finite 1 -element Element of K32((bool REAL))
K32((bool REAL)) is non empty non trivial non finite set
union (rng F) is complex-membered ext-real-membered real-membered Element of K32(REAL)
len F 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
F . 1 is set
F . (len F) is set
rng F is non empty trivial finite 1 -element Element of K32(K32(REAL))
{[.r,s.]} is non empty trivial finite 1 -element set
C is set
union (rng F) is complex-membered ext-real-membered real-membered Element of K32(REAL)
C is ordinal natural ext-real non negative finite cardinal real V65() V66() set
F /. C is complex-membered ext-real-membered real-membered Element of bool REAL
C + 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
lower_bound (F /. C) is ext-real real V65() Element of REAL
F /. (C + 1) is complex-membered ext-real-membered real-membered Element of bool REAL
lower_bound (F /. (C + 1)) is ext-real real V65() Element of REAL
upper_bound (F /. C) is ext-real real V65() Element of REAL
upper_bound (F /. (C + 1)) is ext-real real V65() Element of REAL
C + 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
F /. (C + 2) is complex-membered ext-real-membered real-membered Element of bool REAL
lower_bound (F /. (C + 2)) is ext-real real V65() Element of REAL
G is ordinal natural ext-real non negative finite cardinal real V65() V66() set
F . G is set
C is complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s)))
[#] (Closed-Interval-TSpace (r,s)) is non empty non proper open closed dense non boundary complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s)))
C is Element of K32(K32( the carrier of (Closed-Interval-TSpace (r,s))))
{ b₁ where b₁ is complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s))) : ( b₁ in C & ex b₂ being complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s))) st
( b₂ in C & b₁ c< b₂ ) ) } is set
C \ { b₁ where b₁ is complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s))) : ( b₁ in C & ex b₂ being complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s))) st
( b₂ in C & b₁ c< b₂ ) ) } is Element of K32(K32( the carrier of (Closed-Interval-TSpace (r,s))))
{ b₁ where b₁ is Element of K32(K32( the carrier of (Closed-Interval-TSpace (r,s)))) : ( b₁ is Cover of the carrier of (Closed-Interval-TSpace (r,s)) & b₁ c= C \ { b₁ where b₂ is complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s))) : ( b₁ in C & ex b₃ being complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s))) st
( b₂ in C & b₁ c< b₂ ) ) } ) } is set
RelIncl { b₁ where b₁ is Element of K32(K32( the carrier of (Closed-Interval-TSpace (r,s)))) : ( b₁ is Cover of the carrier of (Closed-Interval-TSpace (r,s)) & b₁ c= C \ { b₁ where b₂ is complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s))) : ( b₁ in C & ex b₃ being complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s))) st
( b₂ in C & b₁ c< b₂ ) ) } ) } is Relation-like reflexive antisymmetric transitive set
{ (lower_bound ].b₁,s.]) where b₁ is ext-real real V65() Element of REAL : ].b₁,s.] in C \ { b₁ where b₂ is complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s))) : ( b₁ in C & ex b₃ being complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s))) st
( b₂ in C & b₁ c< b₂ ) ) } } is set
{ (upper_bound [.r,b₁.[) where b₁ is ext-real real V65() Element of REAL : [.r,b₁.[ in C \ { b₁ where b₂ is complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s))) : ( b₁ in C & ex b₃ being complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s))) st
( b₂ in C & b₁ c< b₂ ) ) } } is set
T is set
LM1 is connected complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s)))
RM1 is complex-membered ext-real-membered real-membered Element of K32(REAL)
{ (upper_bound b₁) where b₁ is complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s))) : b₁ in C \ { b₁ where b₂ is complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s))) : ( b₁ in C & ex b₃ being complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s))) st
( b₂ in C & b₁ c< b₂ ) ) } } is set
RM1 is set
M is ext-real real V65() Element of REAL
[.r,M.[ 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,M.[ is ext-real real V65() Element of REAL
RM1 is set
M is ext-real real V65() Element of REAL
[.r,M.[ 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,M.[ is ext-real real V65() Element of REAL
{ (lower_bound b₁) where b₁ is complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s))) : b₁ in C \ { b₁ where b₂ is complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s))) : ( b₁ in C & ex b₃ being complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s))) st
( b₂ in C & b₁ c< b₂ ) ) } } is set
M is set
C is ext-real real V65() Element of REAL
].C,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 ].C,s.] is ext-real real V65() Element of REAL
M is set
C is ext-real real V65() Element of REAL
].C,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 ].C,s.] is ext-real real V65() Element of REAL
field (RelIncl { b₁ where b₁ is Element of K32(K32( the carrier of (Closed-Interval-TSpace (r,s)))) : ( b₁ is Cover of the carrier of (Closed-Interval-TSpace (r,s)) & b₁ c= C \ { b₁ where b₂ is complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s))) : ( b₁ in C & ex b₃ being complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s))) st
( b₂ in C & b₁ c< b₂ ) ) } ) } ) is set
M is set
C is Element of K32(K32( the carrier of (Closed-Interval-TSpace (r,s))))
union C is complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s)))
R2 is set
R1 is set
R2 is open connected complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s)))
RM is ext-real real V65() set
[.r,RM.[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
R2 is open connected complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s)))
RM is ext-real real V65() set
].RM,s.] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
RM is ext-real real V65() set
].RM,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 ].RM,s.] is ext-real real V65() Element of REAL
R2 is open connected complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s)))
RM is ext-real real V65() set
X is ext-real real V65() set
].RM,X.[ 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)
R2 is open connected complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s)))
R1 is open connected complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s)))
RM is ext-real real V65() set
[.r,RM.[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
RM is ext-real real V65() set
[.r,RM.[ 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,RM.[ is ext-real real V65() Element of REAL
R1 is open connected complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s)))
RM is ext-real real V65() set
].RM,s.] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
R1 is open connected complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s)))
RM is ext-real real V65() set
X is ext-real real V65() set
].RM,X.[ 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)
R1 is open connected complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s)))
X is set
LM is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded Element of K32(REAL)
sup LM is ext-real real V65() set
kL is ext-real real V65() Element of REAL
[.r,kL.[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
b is ext-real real V65() Element of REAL
[.r,b.[ 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,b.[ is ext-real real V65() Element of REAL
union C is complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s)))
LEWY is set
LLEWY is set
upper_bound [.r,kL.[ is ext-real real V65() Element of REAL
lower_bound [.r,kL.[ is ext-real real V65() Element of REAL
LEWY is non empty complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s)))
LLEWY is complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s)))
pP is ext-real real V65() set
].pP,s.] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
pP is ext-real real V65() set
PRAWY is ext-real real V65() set
].pP,PRAWY.[ 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)
pP is ext-real real V65() set
].pP,s.] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
PRAWY is ext-real real V65() set
b is ext-real real V65() set
].PRAWY,b.[ 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)
pP is ext-real real V65() set
[.r,pP.[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
upper_bound LLEWY is ext-real real V65() set
PRAWY is set
b is ext-real real V65() Element of REAL
X is non empty finite Element of K32(K32(REAL))
RM is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded Element of K32(REAL)
inf RM is ext-real real V65() set
pP is ext-real real V65() Element of REAL
].pP,s.] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
b is ext-real real V65() Element of REAL
].b,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 ].b,s.] is ext-real real V65() Element of REAL
lower_bound ].pP,s.] is ext-real real V65() Element of REAL
upper_bound ].pP,s.] is ext-real real V65() Element of REAL
PRAWY is non empty complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s)))
IT is complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s)))
IT is ext-real real V65() set
[.r,IT.[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
IT is ext-real real V65() set
[.r,IT.[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
IT is ext-real real V65() set
].IT,s.] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
IT is ext-real real V65() set
].IT,s.] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
IT is ext-real real V65() set
i is ext-real real V65() set
].IT,i.[ 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)
IT is ext-real real V65() set
i is ext-real real V65() set
].IT,i.[ 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)
i is ext-real real V65() Element of REAL
n is ext-real real V65() Element of REAL
].i,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)
IT is complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s)))
upper_bound IT is ext-real real V65() set
i is ext-real real V65() Element of REAL
IT is ext-real real V65() Element of REAL
].IT,i.[ 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)
T is non empty TopSpace-like connected TopStruct
the carrier of T is non empty set
K32( the carrier of T) is non empty set
IT is complex-membered ext-real-membered real-membered Element of K32(REAL)
card X 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 omega
IT is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
IT is Element of X
i is complex-membered ext-real-membered real-membered Element of K32(REAL)
union X is complex-membered ext-real-membered real-membered Element of K32(REAL)
upper_bound IT is ext-real real V65() Element of REAL
i is set
n is Element of X
LLEWY is Element of X
IT is Relation-like NAT -defined X -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of X
len IT is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
IT . 1 is set
rng IT is finite Element of K32(X)
K32(X) is non empty finite V43() set
IT is Relation-like NAT -defined bool REAL -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool REAL
rng IT is finite Element of K32((bool REAL))
K32((bool REAL)) is non empty non trivial non finite set
dom IT is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of K32(NAT)
IT /. 1 is complex-membered ext-real-membered real-membered Element of bool REAL
IT . 1 is set
i is ordinal natural ext-real non negative finite cardinal real V65() V66() set
IT . i is set
IT /. i is complex-membered ext-real-membered real-membered Element of bool REAL
i is ordinal natural ext-real non negative finite cardinal real V65() V66() set
IT . i is set
IT /. i is complex-membered ext-real-membered real-membered Element of bool REAL
i is ordinal natural ext-real non negative finite cardinal real V65() V66() set
IT /. i is complex-membered ext-real-membered real-membered Element of bool REAL
upper_bound (IT /. i) is ext-real real V65() Element of REAL
i + 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
IT /. (i + 1) is complex-membered ext-real-membered real-membered Element of bool REAL
upper_bound (IT /. (i + 1)) is ext-real real V65() Element of REAL
IT . (i + 1) is set
i is ext-real real V65() Element of the carrier of (Closed-Interval-TSpace (r,s))
len IT is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
IT . i is set
lower_bound (IT /. (i + 1)) is ext-real real V65() Element of REAL
n is Element of X
upper_bound n is ext-real real V65() Element of REAL
n is ordinal natural ext-real non negative finite cardinal real V65() V66() set
IT /. n is complex-membered ext-real-membered real-membered Element of bool REAL
n + 0 is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
n is Element of X
upper_bound n is ext-real real V65() Element of REAL
IT /. 0 is complex-membered ext-real-membered real-membered Element of bool REAL
upper_bound (IT /. 0) is ext-real real V65() Element of REAL
i is ext-real real V65() Element of the carrier of (Closed-Interval-TSpace (r,s))
i is ordinal natural ext-real non negative finite cardinal real V65() V66() set
IT /. i is complex-membered ext-real-membered real-membered Element of bool REAL
upper_bound (IT /. i) is ext-real real V65() Element of REAL
i is ext-real real V65() Element of the carrier of (Closed-Interval-TSpace (r,s))
i is ordinal natural ext-real non negative finite cardinal real V65() V66() set
IT /. i is complex-membered ext-real-membered real-membered Element of bool REAL
i is ordinal natural ext-real non negative finite cardinal real V65() V66() set
IT /. i is complex-membered ext-real-membered real-membered Element of bool REAL
i + 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
IT /. (i + 1) is complex-membered ext-real-membered real-membered Element of bool REAL
IT . (i + 1) is set
IT . i is set
upper_bound (IT /. i) is ext-real real V65() Element of REAL
len IT is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
n is Element of X
upper_bound n is ext-real real V65() Element of REAL
lower_bound (IT /. (i + 1)) is ext-real real V65() Element of REAL
upper_bound (IT /. (i + 1)) is ext-real real V65() Element of REAL
a is ext-real real V65() Element of the carrier of (Closed-Interval-TSpace (r,s))
a is ext-real real V65() Element of the carrier of (Closed-Interval-TSpace (r,s))
(upper_bound n) + (upper_bound (IT /. (i + 1))) is ext-real real V65() Element of REAL
((upper_bound n) + (upper_bound (IT /. (i + 1)))) / 2 is ext-real real V65() Element of REAL
c₄₀ is ext-real real V65() Element of the carrier of (Closed-Interval-TSpace (r,s))
x is ext-real real V65() Element of the carrier of (Closed-Interval-TSpace (r,s))
b is ext-real real V65() Element of the carrier of (Closed-Interval-TSpace (r,s))
c₄₀ is ext-real real V65() Element of the carrier of (Closed-Interval-TSpace (r,s))
a is ext-real real V65() Element of the carrier of (Closed-Interval-TSpace (r,s))
b is ext-real real V65() Element of the carrier of (Closed-Interval-TSpace (r,s))
Seg i is finite i -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of K32(NAT)
IT | (Seg i) is Relation-like Seg i -defined NAT -defined bool REAL -valued Function-like finite FinSubsequence-like Element of K32(K33(NAT,(bool REAL)))
K33(NAT,(bool REAL)) is Relation-like non trivial non finite set
K32(K33(NAT,(bool REAL))) is non empty non trivial non finite set
rng (IT | (Seg i)) is finite Element of K32((bool REAL))
bool the carrier of (Closed-Interval-TSpace (r,s)) is non empty Element of K32(K32( the carrier of (Closed-Interval-TSpace (r,s))))
x is set
x is Element of K32(K32( the carrier of (Closed-Interval-TSpace (r,s))))
union x is complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s)))
x is set
a2 is ext-real real V65() Element of the carrier of (Closed-Interval-TSpace (r,s))
b2 is ordinal natural ext-real non negative finite cardinal real V65() V66() set
IT /. b2 is complex-membered ext-real-membered real-membered Element of bool REAL
IT . b2 is set
a2 is ext-real real V65() Element of the carrier of (Closed-Interval-TSpace (r,s))
a2 is ext-real real V65() Element of the carrier of (Closed-Interval-TSpace (r,s))
[x,M] is set
{x,M} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,M},{x}} is non empty finite V43() set
x is set
i + 0 is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
a2 is ordinal natural ext-real non negative finite cardinal real V65() V66() set
dom (IT | (Seg i)) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of K32((Seg i))
K32((Seg i)) is non empty finite V43() set
card (rng (IT | (Seg i))) is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of omega
card (dom (IT | (Seg i))) is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of omega
i + 0 is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
IT /. 0 is complex-membered ext-real-membered real-membered Element of bool REAL
i is ordinal natural ext-real non negative finite cardinal real V65() V66() set
IT /. i is complex-membered ext-real-membered real-membered Element of bool REAL
i is set
dom IT is finite set
i is set
IT . i is set
IT . i is set
IT /. i is complex-membered ext-real-membered real-membered Element of bool REAL
IT /. i is complex-membered ext-real-membered real-membered Element of bool REAL
a is ordinal natural ext-real non negative finite cardinal real V65() V66() set
n is ordinal natural ext-real non negative finite cardinal real V65() V66() set
IT /. a is complex-membered ext-real-membered real-membered Element of bool REAL
IT /. n is complex-membered ext-real-membered real-membered Element of bool REAL
b is ext-real real V65() Element of the carrier of (Closed-Interval-TSpace (r,s))
n is ordinal natural ext-real non negative finite cardinal real V65() V66() set
a is ordinal natural ext-real non negative finite cardinal real V65() V66() set
IT /. n is complex-membered ext-real-membered real-membered Element of bool REAL
IT /. a is complex-membered ext-real-membered real-membered Element of bool REAL
b is ext-real real V65() Element of the carrier of (Closed-Interval-TSpace (r,s))
a is ordinal natural ext-real non negative finite cardinal real V65() V66() set
n is ordinal natural ext-real non negative finite cardinal real V65() V66() set
i is ordinal natural ext-real non negative finite cardinal real V65() V66() set
i is ordinal natural ext-real non negative finite cardinal real V65() V66() set
IT /. i is complex-membered ext-real-membered real-membered Element of bool REAL
IT /. i is complex-membered ext-real-membered real-membered Element of bool REAL
IT . i is set
IT . i is set
i is complex-membered ext-real-membered real-membered Element of K32( the carrier of (Closed-Interval-TSpace (r,s)))
i is ext-real real V65() set
[.r,i.[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
i is ext-real real V65() set
n is ext-real real V65() set
].i,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)
i is ext-real real V65() set
[.r,i.[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
n is ext-real real V65() set
a is ext-real real V65() set
].n,a.[ 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)
i is ext-real real V65() set
].i,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 i is ext-real real V65() set
n is set
a is ext-real real V65() Element of REAL
union (rng IT) is complex-membered ext-real-membered real-membered Element of K32(REAL)
len IT is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
IT . (len IT) is set
Seg (len IT) is finite len IT -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of K32(NAT)
card (dom IT) is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of omega
K33((dom IT),X) is Relation-like finite set
K32(K33((dom IT),X)) is non empty finite V43() set
i is set
i is set
IT . i is set
i is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
IT /. i is complex-membered ext-real-membered real-membered Element of bool REAL
IT . i is set
i + 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
IT . (i + 1) is set
0 + 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
IT /. (i + 1) is complex-membered ext-real-membered real-membered Element of bool REAL
i + 0 is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
n is Element of X
upper_bound n is ext-real real V65() Element of REAL
n is ordinal natural ext-real non negative finite cardinal real V65() V66() set
IT /. n is complex-membered ext-real-membered real-membered Element of bool REAL
IT . n is set
a is ext-real real V65() set
[.r,a.[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
a is ext-real real V65() set
[.r,a.[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
a is ext-real real V65() set
].a,s.] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
a is ext-real real V65() set
].a,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 ].a,s.] is ext-real real V65() Element of REAL
a is ext-real real V65() set
b is ext-real real V65() set
].a,b.[ 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)
a is ext-real real V65() set
b is ext-real real V65() set
].a,b.[ 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)
c₄₀ is ext-real real V65() Element of REAL
x is ext-real real V65() Element of REAL
].c₄₀,x.[ 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 ordinal natural ext-real non negative finite cardinal real V65() V66() set
a is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
IT /. n is complex-membered ext-real-membered real-membered Element of bool REAL
IT . n is set
n + 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
IT . (n + 1) is set
a + 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
IT /. (a + 1) is complex-membered ext-real-membered real-membered Element of bool REAL
IT . (a + 1) is set
IT /. (n + 1) is complex-membered ext-real-membered real-membered Element of bool REAL
n + 0 is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
union X is complex-membered ext-real-membered real-membered Element of K32(REAL)
upper_bound (IT /. n) is ext-real real V65() Element of REAL
upper_bound (IT /. (n + 1)) is ext-real real V65() Element of REAL
b is Element of X
upper_bound b is ext-real real V65() Element of REAL
lower_bound (IT /. n) is ext-real real V65() Element of REAL
lower_bound (IT /. (n + 1)) is ext-real real V65() Element of REAL
b is Element of X
upper_bound b is ext-real real V65() Element of REAL
b is Element of X
upper_bound b is ext-real real V65() Element of REAL
b is ext-real real V65() Element of REAL
c₄₀ is ext-real real V65() Element of REAL
].b,c₄₀.[ 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)
x is Element of X
upper_bound x is ext-real real V65() Element of REAL
n is ordinal natural ext-real non negative finite cardinal real V65() V66() set
IT /. n is complex-membered ext-real-membered real-membered Element of bool REAL
n + 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
lower_bound (IT /. n) is ext-real real V65() Element of REAL
IT /. (n + 1) is complex-membered ext-real-membered real-membered Element of bool REAL
lower_bound (IT /. (n + 1)) is ext-real real V65() Element of REAL
upper_bound (IT /. n) is ext-real real V65() Element of REAL
upper_bound (IT /. (n + 1)) is ext-real real V65() Element of REAL
n + 0 is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
a is ordinal natural ext-real non negative finite cardinal real V65() V66() set
a + 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
n + 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
(n + 1) + 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
IT . (n + 1) is set
IT /. ((n + 1) + 1) is complex-membered ext-real-membered real-membered Element of bool REAL
upper_bound (IT /. ((n + 1) + 1)) is ext-real real V65() Element of REAL
IT /. (n + 2) is complex-membered ext-real-membered real-membered Element of bool REAL
lower_bound (IT /. (n + 2)) is ext-real real V65() Element of REAL
b is ext-real real V65() Element of REAL
c₄₀ is ext-real real V65() Element of REAL
].b,c₄₀.[ 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)
lower_bound ].b,c₄₀.[ is ext-real real V65() Element of REAL
upper_bound ].b,c₄₀.[ is ext-real real V65() Element of REAL
(IT /. n) \/ (IT /. (n + 2)) is complex-membered ext-real-membered real-membered Element of K32(REAL)
x is set
x is ext-real real V65() Element of REAL
a2 is ext-real real V65() Element of REAL
b2 is ext-real real V65() Element of REAL
].a2,b2.[ 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)
a2 is ext-real real V65() Element of REAL
b2 is ext-real real V65() Element of REAL
].a2,b2.[ 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)
upper_bound ].a2,b2.[ is ext-real real V65() Element of REAL
lower_bound ].a2,b2.[ is ext-real real V65() Element of REAL
a + 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
IT . (n + 2) is set
IT . n is set
upper_bound LEWY is ext-real real V65() set
upper_bound [.r,s.] is ext-real real V65() Element of REAL
lower_bound [.r,s.] is ext-real real V65() Element of REAL
lower_bound PRAWY is ext-real real V65() set
n is ordinal natural ext-real non negative finite cardinal real V65() V66() set
IT . n is set
IT /. n is complex-membered ext-real-membered real-membered Element of bool REAL
a is ext-real real V65() Element of REAL
b is ext-real real V65() Element of REAL
].a,b.[ 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
Closed-Interval-TSpace (r,s) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (r,s)) is non empty complex-membered ext-real-membered real-membered set
K32( the carrier of (Closed-Interval-TSpace (r,s))) is non empty set
K32(K32( the carrier of (Closed-Interval-TSpace (r,s)))) is non empty 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 Relation-like NAT -defined K32(REAL) -valued Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of K32(REAL)
n is Element of K32(K32( the carrier of (Closed-Interval-TSpace (r,s))))
len <*[.r,s.]*> 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
C is ordinal natural ext-real non negative finite cardinal real V65() V66() set
<*[.r,s.]*> /. C is complex-membered ext-real-membered real-membered Element of K32(REAL)
C + 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
lower_bound (<*[.r,s.]*> /. C) is ext-real real V65() Element of REAL
<*[.r,s.]*> /. (C + 1) is complex-membered ext-real-membered real-membered Element of K32(REAL)
lower_bound (<*[.r,s.]*> /. (C + 1)) is ext-real real V65() Element of REAL
upper_bound (<*[.r,s.]*> /. C) is ext-real real V65() Element of REAL
upper_bound (<*[.r,s.]*> /. (C + 1)) is ext-real real V65() Element of REAL
C + 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
<*[.r,s.]*> /. (C + 2) is complex-membered ext-real-membered real-membered Element of K32(REAL)
lower_bound (<*[.r,s.]*> /. (C + 2)) is ext-real real V65() Element of REAL
rng <*[.r,s.]*> is non empty trivial finite 1 -element Element of K32(K32(REAL))
union (rng <*[.r,s.]*>) is complex-membered ext-real-membered real-membered Element of K32(REAL)
r is ext-real real V65() set
Closed-Interval-TSpace (r,r) is non empty trivial finite 1 -element strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (r,r)) is non empty trivial finite 1 -element complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
K32( the carrier of (Closed-Interval-TSpace (r,r))) is non empty finite V43() set
K32(K32( the carrier of (Closed-Interval-TSpace (r,r)))) is non empty finite V43() set
[.r,r.] is non empty complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
<*[.r,r.]*> is Relation-like NAT -defined K32(REAL) -valued Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of K32(REAL)
n is finite V43() Element of K32(K32( the carrier of (Closed-Interval-TSpace (r,r))))
F is Relation-like NAT -defined bool REAL -valued Function-like finite FinSequence-like FinSubsequence-like (r,r,n)
{r} is non empty trivial finite 1 -element complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded Element of K32(REAL)
r is ext-real real V65() set
s is ext-real real V65() set
Closed-Interval-TSpace (r,s) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (r,s)) is non empty complex-membered ext-real-membered real-membered set
K32( the carrier of (Closed-Interval-TSpace (r,s))) is non empty set
K32(K32( the carrier of (Closed-Interval-TSpace (r,s)))) is non empty set
n is Element of K32(K32( the carrier of (Closed-Interval-TSpace (r,s))))
F is Relation-like NAT -defined bool REAL -valued Function-like finite FinSequence-like FinSubsequence-like (r,s,n)
len F is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
(len F) + 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
0 + 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
rng F is finite Element of K32((bool REAL))
K32((bool REAL)) is non empty non trivial non finite set
union (rng F) is complex-membered ext-real-membered real-membered 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)
r is ext-real real V65() set
s is ext-real real V65() set
Closed-Interval-TSpace (r,s) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (r,s)) is non empty complex-membered ext-real-membered real-membered set
K32( the carrier of (Closed-Interval-TSpace (r,s))) is non empty set
K32(K32( the carrier of (Closed-Interval-TSpace (r,s)))) is non empty 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 Relation-like NAT -defined K32(REAL) -valued Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of K32(REAL)
n is Element of K32(K32( the carrier of (Closed-Interval-TSpace (r,s))))
F is Relation-like NAT -defined bool REAL -valued Function-like finite FinSequence-like FinSubsequence-like (r,s,n)
len F is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
rng F is finite Element of K32((bool REAL))
K32((bool REAL)) is non empty non trivial non finite set
union (rng F) is complex-membered ext-real-membered real-membered Element of K32(REAL)
dom F is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of K32(NAT)
F . 1 is set
C is set
C is set
{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 Element of K32(REAL)
G is set
L is set
F . L is set
r is ext-real real V65() set
s is ext-real real V65() set
Closed-Interval-TSpace (r,s) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (r,s)) is non empty complex-membered ext-real-membered real-membered set
K32( the carrier of (Closed-Interval-TSpace (r,s))) is non empty set
K32(K32( the carrier of (Closed-Interval-TSpace (r,s)))) is non empty set
n is ordinal natural ext-real non negative finite cardinal real V65() V66() set
F is ordinal natural ext-real non negative finite cardinal real V65() V66() set
C is Element of K32(K32( the carrier of (Closed-Interval-TSpace (r,s))))
G is Relation-like NAT -defined bool REAL -valued Function-like finite FinSequence-like FinSubsequence-like (r,s,C)
dom G is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of K32(NAT)
G /. n is complex-membered ext-real-membered real-membered Element of bool REAL
lower_bound (G /. n) is ext-real real V65() Element of REAL
G /. F is complex-membered ext-real-membered real-membered Element of bool REAL
lower_bound (G /. F) is ext-real real V65() Element of REAL
L is ordinal natural ext-real non negative finite cardinal real V65() V66() set
G /. L is complex-membered ext-real-membered real-membered Element of bool REAL
lower_bound (G /. L) is ext-real real V65() Element of REAL
L + 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
G /. (L + 1) is complex-membered ext-real-membered real-membered Element of bool REAL
lower_bound (G /. (L + 1)) is ext-real real V65() Element of REAL
len G is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
G /. 0 is complex-membered ext-real-membered real-membered Element of bool REAL
lower_bound (G /. 0) is ext-real real V65() Element of REAL
r is ext-real real V65() set
s is ext-real real V65() set
Closed-Interval-TSpace (r,s) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (r,s)) is non empty complex-membered ext-real-membered real-membered set
K32( the carrier of (Closed-Interval-TSpace (r,s))) is non empty set
K32(K32( the carrier of (Closed-Interval-TSpace (r,s)))) is non empty set
n is ordinal natural ext-real non negative finite cardinal real V65() V66() set
F is ordinal natural ext-real non negative finite cardinal real V65() V66() set
C is Element of K32(K32( the carrier of (Closed-Interval-TSpace (r,s))))
G is Relation-like NAT -defined bool REAL -valued Function-like finite FinSequence-like FinSubsequence-like (r,s,C)
dom G is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of K32(NAT)
G /. n is complex-membered ext-real-membered real-membered Element of bool REAL
upper_bound (G /. n) is ext-real real V65() Element of REAL
G /. F is complex-membered ext-real-membered real-membered Element of bool REAL
upper_bound (G /. F) is ext-real real V65() Element of REAL
L is ordinal natural ext-real non negative finite cardinal real V65() V66() set
G /. L is complex-membered ext-real-membered real-membered Element of bool REAL
upper_bound (G /. L) is ext-real real V65() Element of REAL
L + 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
G /. (L + 1) is complex-membered ext-real-membered real-membered Element of bool REAL
upper_bound (G /. (L + 1)) is ext-real real V65() Element of REAL
len G is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
G /. 0 is complex-membered ext-real-membered real-membered Element of bool REAL
upper_bound (G /. 0) is ext-real real V65() Element of REAL
r is ext-real real V65() set
s is ext-real real V65() set
Closed-Interval-TSpace (r,s) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (r,s)) is non empty complex-membered ext-real-membered real-membered set
K32( the carrier of (Closed-Interval-TSpace (r,s))) is non empty set
K32(K32( the carrier of (Closed-Interval-TSpace (r,s)))) is non empty set
n is ordinal natural ext-real non negative finite cardinal real V65() V66() set
n + 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
F is Element of K32(K32( the carrier of (Closed-Interval-TSpace (r,s))))
C is Relation-like NAT -defined bool REAL -valued Function-like finite FinSequence-like FinSubsequence-like (r,s,F)
len C is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
C /. (n + 1) is complex-membered ext-real-membered real-membered Element of bool REAL
lower_bound (C /. (n + 1)) is ext-real real V65() Element of REAL
C /. n is complex-membered ext-real-membered real-membered Element of bool REAL
upper_bound (C /. n) is ext-real real V65() Element of REAL
].(lower_bound (C /. (n + 1))),(upper_bound (C /. 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)
r is ext-real real V65() set
s is ext-real real V65() set
Closed-Interval-TSpace (r,s) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (r,s)) is non empty complex-membered ext-real-membered real-membered set
K32( the carrier of (Closed-Interval-TSpace (r,s))) is non empty set
K32(K32( the carrier of (Closed-Interval-TSpace (r,s)))) is non empty set
n is Element of K32(K32( the carrier of (Closed-Interval-TSpace (r,s))))
F is Relation-like NAT -defined bool REAL -valued Function-like finite FinSequence-like FinSubsequence-like (r,s,n)
F /. 1 is complex-membered ext-real-membered real-membered Element of bool REAL
lower_bound (F /. 1) is ext-real real V65() Element of REAL
len F is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
F . 1 is 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 Relation-like NAT -defined K32(REAL) -valued Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence 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)
C is ext-real real V65() set
[.r,C.[ 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 closed 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
Closed-Interval-TSpace (r,s) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (r,s)) is non empty complex-membered ext-real-membered real-membered set
K32( the carrier of (Closed-Interval-TSpace (r,s))) is non empty set
K32(K32( the carrier of (Closed-Interval-TSpace (r,s)))) is non empty set
n is Element of K32(K32( the carrier of (Closed-Interval-TSpace (r,s))))
F is Relation-like NAT -defined bool REAL -valued Function-like finite FinSequence-like FinSubsequence-like (r,s,n)
F /. 1 is complex-membered ext-real-membered real-membered Element of bool REAL
len F is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
F . 1 is 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 Relation-like NAT -defined K32(REAL) -valued Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence 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)
C is ext-real real V65() set
[.r,C.[ 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 closed 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
Closed-Interval-TSpace (r,s) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (r,s)) is non empty complex-membered ext-real-membered real-membered set
K32( the carrier of (Closed-Interval-TSpace (r,s))) is non empty set
K32(K32( the carrier of (Closed-Interval-TSpace (r,s)))) is non empty set
n is Element of K32(K32( the carrier of (Closed-Interval-TSpace (r,s))))
F is Relation-like NAT -defined bool REAL -valued Function-like finite FinSequence-like FinSubsequence-like (r,s,n)
len F is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
F /. (len F) is complex-membered ext-real-membered real-membered Element of bool REAL
upper_bound (F /. (len F)) is ext-real real V65() Element of REAL
F . (len F) is 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 Relation-like NAT -defined K32(REAL) -valued Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of K32(REAL)
F /. 1 is complex-membered ext-real-membered real-membered Element of bool REAL
[.r,s.] 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
].C,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 closed 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
Closed-Interval-TSpace (r,s) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (r,s)) is non empty complex-membered ext-real-membered real-membered set
K32( the carrier of (Closed-Interval-TSpace (r,s))) is non empty set
K32(K32( the carrier of (Closed-Interval-TSpace (r,s)))) is non empty set
n is Element of K32(K32( the carrier of (Closed-Interval-TSpace (r,s))))
F is Relation-like NAT -defined bool REAL -valued Function-like finite FinSequence-like FinSubsequence-like (r,s,n)
len F is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
F /. (len F) is complex-membered ext-real-membered real-membered Element of bool REAL
F . (len F) is 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 Relation-like NAT -defined K32(REAL) -valued Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of K32(REAL)
F /. 1 is complex-membered ext-real-membered real-membered Element of bool REAL
[.r,s.] 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
].C,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 closed 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
Closed-Interval-TSpace (r,s) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (r,s)) is non empty complex-membered ext-real-membered real-membered set
K32( the carrier of (Closed-Interval-TSpace (r,s))) is non empty set
K32(K32( the carrier of (Closed-Interval-TSpace (r,s)))) is non empty set
n is Element of K32(K32( the carrier of (Closed-Interval-TSpace (r,s))))
F is Relation-like NAT -defined bool REAL -valued Function-like finite FinSequence-like FinSubsequence-like (r,s,n)
len F is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
(len F) + 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
0 + 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
Seg ((len F) + 1) is non empty finite (len F) + 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)
k is ordinal natural ext-real non negative finite cardinal real V65() V66() set
F /. k is complex-membered ext-real-membered real-membered Element of bool REAL
lower_bound (F /. k) is ext-real real V65() Element of REAL
k - 1 is ext-real real V65() V66() Element of REAL
F /. (k - 1) is complex-membered ext-real-membered real-membered Element of bool REAL
upper_bound (F /. (k - 1)) is ext-real real V65() Element of REAL
].(lower_bound (F /. k)),(upper_bound (F /. (k - 1))).[ 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)
(len F) + 0 is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
G is ext-real real V65() Element of REAL
L is ext-real real V65() Element of REAL
1 - 1 is ext-real real V65() V66() Element of REAL
(k - 1) + 1 is ext-real real V65() V66() Element of REAL
F /. ((k - 1) + 1) is complex-membered ext-real-membered real-membered Element of bool REAL
lower_bound (F /. ((k - 1) + 1)) is ext-real real V65() Element of REAL
].(lower_bound (F /. ((k - 1) + 1))),(upper_bound (F /. (k - 1))).[ 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)
z is set
x is ext-real real V65() Element of REAL
G is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V124() V125() V126() FinSequence of REAL
dom G is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of K32(NAT)
len G is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
G . 1 is ext-real real V65() set
G . (len G) is ext-real real V65() set
L is ordinal natural ext-real non negative finite cardinal real V65() V66() set
L + 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
G . (L + 1) is ext-real real V65() set
F /. (L + 1) is complex-membered ext-real-membered real-membered Element of bool REAL
lower_bound (F /. (L + 1)) is ext-real real V65() Element of REAL
F /. L is complex-membered ext-real-membered real-membered Element of bool REAL
upper_bound (F /. L) is ext-real real V65() Element of REAL
].(lower_bound (F /. (L + 1))),(upper_bound (F /. L)).[ 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)
1 + 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
(L + 1) - 1 is ext-real real V65() V66() Element of REAL
F /. ((L + 1) - 1) is complex-membered ext-real-membered real-membered Element of bool REAL
upper_bound (F /. ((L + 1) - 1)) is ext-real real V65() Element of REAL
].(lower_bound (F /. (L + 1))),(upper_bound (F /. ((L + 1) - 1))).[ 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
Closed-Interval-TSpace (r,s) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (r,s)) is non empty complex-membered ext-real-membered real-membered set
K32( the carrier of (Closed-Interval-TSpace (r,s))) is non empty set
K32(K32( the carrier of (Closed-Interval-TSpace (r,s)))) is non empty set
n is Element of K32(K32( the carrier of (Closed-Interval-TSpace (r,s))))
F is Relation-like NAT -defined bool REAL -valued Function-like finite FinSequence-like FinSubsequence-like (r,s,n)
C is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V124() V125() V126() (r,s,n,F)
len C is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
len F is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
1 + 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
(len F) + 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
r is ext-real real V65() set
s is ext-real real V65() set
Closed-Interval-TSpace (r,s) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (r,s)) is non empty complex-membered ext-real-membered real-membered set
K32( the carrier of (Closed-Interval-TSpace (r,s))) is non empty set
K32(K32( the carrier of (Closed-Interval-TSpace (r,s)))) is non empty set
<*r,s*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like set
n is Element of K32(K32( the carrier of (Closed-Interval-TSpace (r,s))))
F is Relation-like NAT -defined bool REAL -valued Function-like finite FinSequence-like FinSubsequence-like (r,s,n)
len F is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
C is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V124() V125() V126() (r,s,n,F)
C . 1 is ext-real real V65() set
len C is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
(len F) + 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
C . 2 is ext-real real V65() set
r is ext-real real V65() set
s is ext-real real V65() set
Closed-Interval-TSpace (r,s) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (r,s)) is non empty complex-membered ext-real-membered real-membered set
K32( the carrier of (Closed-Interval-TSpace (r,s))) is non empty set
K32(K32( the carrier of (Closed-Interval-TSpace (r,s)))) is non empty set
n is ordinal natural ext-real non negative finite cardinal real V65() V66() set
n + 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
F is Element of K32(K32( the carrier of (Closed-Interval-TSpace (r,s))))
C is Relation-like NAT -defined bool REAL -valued Function-like finite FinSequence-like FinSubsequence-like (r,s,F)
C /. n is complex-membered ext-real-membered real-membered Element of bool REAL
upper_bound (C /. n) is ext-real real V65() Element of REAL
G is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V124() V125() V126() (r,s,F,C)
len G is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
G . (n + 1) is ext-real real V65() set
C /. (n + 1) is complex-membered ext-real-membered real-membered Element of bool REAL
lower_bound (C /. (n + 1)) is ext-real real V65() Element of REAL
].(lower_bound (C /. (n + 1))),(upper_bound (C /. 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)
r is ext-real real V65() set
s is ext-real real V65() set
Closed-Interval-TSpace (r,s) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (r,s)) is non empty complex-membered ext-real-membered real-membered set
K32( the carrier of (Closed-Interval-TSpace (r,s))) is non empty set
K32(K32( the carrier of (Closed-Interval-TSpace (r,s)))) is non empty set
n is ordinal natural ext-real non negative finite cardinal real V65() V66() set
F is Element of K32(K32( the carrier of (Closed-Interval-TSpace (r,s))))
C is Relation-like NAT -defined bool REAL -valued Function-like finite FinSequence-like FinSubsequence-like (r,s,F)
len C is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
C /. n is complex-membered ext-real-membered real-membered Element of bool REAL
lower_bound (C /. n) is ext-real real V65() Element of REAL
G is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V124() V125() V126() (r,s,F,C)
G . n is ext-real real V65() set
n -' 1 is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
len G is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
(len C) + 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
1 - 1 is ext-real real V65() V66() Element of REAL
n - 1 is ext-real real V65() V66() Element of REAL
(n -' 1) + 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
G . ((n -' 1) + 1) is ext-real real V65() set
C /. ((n -' 1) + 1) is complex-membered ext-real-membered real-membered Element of bool REAL
lower_bound (C /. ((n -' 1) + 1)) is ext-real real V65() Element of REAL
C /. (n -' 1) is complex-membered ext-real-membered real-membered Element of bool REAL
upper_bound (C /. (n -' 1)) is ext-real real V65() Element of REAL
].(lower_bound (C /. ((n -' 1) + 1))),(upper_bound (C /. (n -' 1))).[ 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
Closed-Interval-TSpace (r,s) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (r,s)) is non empty complex-membered ext-real-membered real-membered set
K32( the carrier of (Closed-Interval-TSpace (r,s))) is non empty set
K32(K32( the carrier of (Closed-Interval-TSpace (r,s)))) is non empty set
n is ordinal natural ext-real non negative finite cardinal real V65() V66() set
n + 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
F is Element of K32(K32( the carrier of (Closed-Interval-TSpace (r,s))))
C is Relation-like NAT -defined bool REAL -valued Function-like finite FinSequence-like FinSubsequence-like (r,s,F)
len C is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
C /. (n + 1) is complex-membered ext-real-membered real-membered Element of bool REAL
lower_bound (C /. (n + 1)) is ext-real real V65() Element of REAL
G is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V124() V125() V126() (r,s,F,C)
G . n is ext-real real V65() set
n -' 1 is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
0 + 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
G . 1 is ext-real real V65() set
rng C is finite Element of K32((bool REAL))
K32((bool REAL)) is non empty non trivial non finite set
1 + 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
dom C is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of K32(NAT)
C . 2 is set
C /. 2 is complex-membered ext-real-membered real-membered Element of bool REAL
[.r,s.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
n - 1 is ext-real real V65() V66() Element of REAL
1 - 1 is ext-real real V65() V66() Element of REAL
0 + 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
len G is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
(len C) + 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
(len G) - 1 is ext-real real V65() V66() Element of REAL
((len G) - 1) + 1 is ext-real real V65() V66() Element of REAL
n - 0 is ext-real non negative real V65() V66() Element of REAL
(n -' 1) + 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
C /. (n -' 1) is complex-membered ext-real-membered real-membered Element of bool REAL
upper_bound (C /. (n -' 1)) is ext-real real V65() Element of REAL
G . ((n -' 1) + 1) is ext-real real V65() set
(n -' 1) + 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
C /. ((n -' 1) + 2) is complex-membered ext-real-membered real-membered Element of bool REAL
lower_bound (C /. ((n -' 1) + 2)) is ext-real real V65() Element of REAL
r is ext-real real V65() set
s is ext-real real V65() set
Closed-Interval-TSpace (r,s) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (r,s)) is non empty complex-membered ext-real-membered real-membered set
K32( the carrier of (Closed-Interval-TSpace (r,s))) is non empty set
K32(K32( the carrier of (Closed-Interval-TSpace (r,s)))) is non empty set
n is Element of K32(K32( the carrier of (Closed-Interval-TSpace (r,s))))
F is Relation-like NAT -defined bool REAL -valued Function-like finite FinSequence-like FinSubsequence-like (r,s,n)
C is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V124() V125() V126() (r,s,n,F)
G is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
dom C is finite set
L is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
K616(C,L) is ext-real real V65() Element of REAL
K616(C,G) is ext-real real V65() Element of REAL
dom C is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of K32(NAT)
C . G is ext-real real V65() set
len C is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
len F is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
(len F) + 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
k is ordinal natural ext-real non negative finite cardinal real V65() V66() set
C . k is ext-real real V65() set
k + 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
C . (k + 1) is ext-real real V65() set
k + 0 is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
F /. (k + 1) is complex-membered ext-real-membered real-membered Element of bool REAL
lower_bound (F /. (k + 1)) is ext-real real V65() Element of REAL
F /. k is complex-membered ext-real-membered real-membered Element of bool REAL
upper_bound (F /. k) is ext-real real V65() Element of REAL
].(lower_bound (F /. (k + 1))),(upper_bound (F /. 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)
1 + 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
C . 2 is ext-real real V65() set
F /. 2 is complex-membered ext-real-membered real-membered Element of bool REAL
lower_bound (F /. 2) is ext-real real V65() Element of REAL
C . 1 is ext-real real V65() set
F /. (1 + 1) is complex-membered ext-real-membered real-membered Element of bool REAL
lower_bound (F /. (1 + 1)) is ext-real real V65() Element of REAL
<*r,s*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like set
C . 1 is ext-real real V65() set
C . 2 is ext-real real V65() set
G -' 1 is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
1 - 1 is ext-real real V65() V66() Element of REAL
G - 1 is ext-real real V65() V66() Element of REAL
(G -' 1) + 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
1 + 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
(1 + 1) - 1 is ext-real real V65() V66() Element of REAL
F /. (G -' 1) is complex-membered ext-real-membered real-membered Element of bool REAL
rng F is finite Element of K32((bool REAL))
K32((bool REAL)) is non empty non trivial non finite set
dom F is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of K32(NAT)
F . (G -' 1) is set
[.r,s.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
upper_bound (F /. (G -' 1)) is ext-real real V65() Element of REAL
C . 0 is ext-real real V65() set
r is ext-real real V65() set
s is ext-real real V65() set
Closed-Interval-TSpace (r,s) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (r,s)) is non empty complex-membered ext-real-membered real-membered set
K32( the carrier of (Closed-Interval-TSpace (r,s))) is non empty set
K32(K32( the carrier of (Closed-Interval-TSpace (r,s)))) is non empty set
n is ordinal natural ext-real non negative finite cardinal real V65() V66() set
n + 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
F is Element of K32(K32( the carrier of (Closed-Interval-TSpace (r,s))))
C is Relation-like NAT -defined bool REAL -valued Function-like finite FinSequence-like FinSubsequence-like (r,s,F)
C . n is set
G is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V124() V125() V126() (r,s,F,C)
len G is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
G . n is ext-real real V65() set
G . (n + 1) is ext-real real V65() set
[.(G . n),(G . (n + 1)).] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
len C is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
(len C) + 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
C /. n is complex-membered ext-real-membered real-membered Element of bool REAL
dom C is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of K32(NAT)
rng C is finite Element of K32((bool REAL))
K32((bool REAL)) is non empty non trivial non finite set
0 + 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
dom G is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of K32(NAT)
n + 0 is ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
[.r,r.] is non empty complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)
<*[.r,r.]*> is Relation-like NAT -defined K32(REAL) -valued Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of K32(REAL)
<*r,s*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like set
G . 1 is ext-real real V65() set
G . 2 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 Relation-like NAT -defined K32(REAL) -valued Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of K32(REAL)
<*r,s*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like set
G . 1 is ext-real real V65() set
G . 2 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 Relation-like NAT -defined K32(REAL) -valued Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of K32(REAL)
1 + 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
G . (1 + 1) is ext-real real V65() set
C /. (1 + 1) is complex-membered ext-real-membered real-membered Element of bool REAL
lower_bound (C /. (1 + 1)) is ext-real real V65() Element of REAL
C /. 1 is complex-membered ext-real-membered real-membered Element of bool REAL
upper_bound (C /. 1) is ext-real real V65() Element of REAL
].(lower_bound (C /. (1 + 1))),(upper_bound (C /. 1)).[ 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 . 2 is ext-real real V65() set
lower_bound (C /. 1) is ext-real real V65() Element of REAL
lower_bound (C /. n) is ext-real real V65() Element of REAL
G . 1 is ext-real real V65() set
upper_bound (C /. n) is ext-real real V65() Element of REAL
n - 1 is ext-real real V65() V66() Element of REAL
1 - 1 is ext-real real V65() V66() Element of REAL
(n - 1) + 1 is ext-real real V65() V66() Element of REAL
G . ((n - 1) + 1) is ext-real real V65() set
C /. ((n - 1) + 1) is complex-membered ext-real-membered real-membered Element of bool REAL
lower_bound (C /. ((n - 1) + 1)) is ext-real real V65() Element of REAL
C /. (n - 1) is complex-membered ext-real-membered real-membered Element of bool REAL
upper_bound (C /. (n - 1)) is ext-real real V65() Element of REAL
].(lower_bound (C /. ((n - 1) + 1))),(upper_bound (C /. (n - 1))).[ 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)
upper_bound (C /. ((n - 1) + 1)) is ext-real real V65() Element of REAL
upper_bound (C /. n) is ext-real real V65() Element of REAL
G . (len G) is ext-real real V65() set
lower_bound (C /. n) is ext-real real V65() Element of REAL
upper_bound (C /. n) is ext-real real V65() Element of REAL
lower_bound (C /. n) is ext-real real V65() Element of REAL
1 + 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