REAL is non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval set
NAT is V106() V107() V108() V109() V110() V111() V112() bounded_below Element of bool REAL
bool REAL is non empty set
omega is V106() V107() V108() V109() V110() V111() V112() bounded_below set
bool omega is non empty set
bool NAT is non empty set
1 is non empty natural V11() ext-real positive non negative real V106() V107() V108() V109() V110() V111() left_end bounded_below Element of NAT
[:1,1:] is non empty set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty set
bool [:[:1,1:],1:] is non empty set
[:[:1,1:],REAL:] is non empty set
bool [:[:1,1:],REAL:] is non empty set
[:REAL,REAL:] is non empty set
[:[:REAL,REAL:],REAL:] is non empty set
bool [:[:REAL,REAL:],REAL:] is non empty set
2 is non empty natural V11() ext-real positive non negative real V106() V107() V108() V109() V110() V111() left_end bounded_below Element of NAT
[:2,2:] is non empty set
[:[:2,2:],REAL:] is non empty set
bool [:[:2,2:],REAL:] is non empty set
{} is empty finite V48() V106() V107() V108() V109() V110() V111() V112() bounded_below bounded_above real-bounded interval set
0 is empty natural V11() ext-real non positive non negative finite V48() real V106() V107() V108() V109() V110() V111() V112() bounded_below bounded_above real-bounded interval Element of NAT
a is Relation-like Function-like FinSequence-like set
dom a is V106() V107() V108() V109() V110() V111() bounded_below Element of bool NAT
M is natural V11() ext-real real set
M + 1 is natural V11() ext-real real V106() V107() V108() V109() V110() V111() bounded_below Element of NAT
len a is natural V11() ext-real real V106() V107() V108() V109() V110() V111() bounded_below Element of NAT
a is Relation-like Function-like FinSequence-like set
dom a is V106() V107() V108() V109() V110() V111() bounded_below Element of bool NAT
M is natural V11() ext-real real set
R is natural V11() ext-real real set
a . M is set
a . R is set
x is natural V11() ext-real real set
a . x is set
x + 1 is natural V11() ext-real real V106() V107() V108() V109() V110() V111() bounded_below Element of NAT
a . (x + 1) is set
y is natural V11() ext-real real set
a . y is set
a . 1 is set
x1 is natural V11() ext-real real set
a . x1 is set
x1 + 1 is natural V11() ext-real real V106() V107() V108() V109() V110() V111() bounded_below Element of NAT
a . (x1 + 1) is set
a . 0 is set
a . 0 is set
x is natural V11() ext-real real set
a . x is set
a is set
[:a,a:] is set
bool [:a,a:] is non empty set
M is Relation-like a -defined a -valued Element of bool [:a,a:]
dom M is Element of bool a
bool a is non empty set
R is set
[R,R] is set
{R,R} is non empty finite set
{R} is non empty finite set
{{R,R},{R}} is non empty finite V48() set
a is set
[:a,a:] is set
bool [:a,a:] is non empty set
M is Relation-like a -defined a -valued Element of bool [:a,a:]
rng M is Element of bool a
bool a is non empty set
R is set
x is set
[x,R] is set
{x,R} is non empty finite set
{x} is non empty finite set
{{x,R},{x}} is non empty finite V48() set
a is set
[:a,a:] is set
bool [:a,a:] is non empty set
M is Relation-like a -defined a -valued Element of bool [:a,a:]
M [*] is Relation-like set
R is set
[R,R] is set
{R,R} is non empty finite set
{R} is non empty finite set
{{R,R},{R}} is non empty finite V48() set
a is set
[:a,a:] is set
bool [:a,a:] is non empty set
M is set
R is set
[M,R] is set
{M,R} is non empty finite set
{M} is non empty finite set
{{M,R},{M}} is non empty finite V48() set
x is Relation-like a -defined a -valued Element of bool [:a,a:]
x [*] is Relation-like set
a is set
[:a,a:] is set
bool [:a,a:] is non empty set
M is Relation-like a -defined a -valued Element of bool [:a,a:]
M [*] is Relation-like set
R is set
x is set
[R,x] is set
{R,x} is non empty finite set
{R} is non empty finite set
{{R,x},{R}} is non empty finite V48() set
field M is set
y is Relation-like Function-like FinSequence-like set
len y is natural V11() ext-real real V106() V107() V108() V109() V110() V111() bounded_below Element of NAT
y . 1 is set
y . (len y) is set
Rev y is Relation-like Function-like FinSequence-like set
x1 is Relation-like Function-like FinSequence-like set
y1 is natural V11() ext-real real set
len x1 is natural V11() ext-real real V106() V107() V108() V109() V110() V111() bounded_below Element of NAT
(len y) - 0 is V11() ext-real real set
(len y) - y1 is V11() ext-real real set
Seg (len y) is V106() V107() V108() V109() V110() V111() bounded_below Element of bool NAT
dom y is V106() V107() V108() V109() V110() V111() bounded_below Element of bool NAT
x1 . y1 is set
((len y) - y1) + 1 is V11() ext-real real set
y . (((len y) - y1) + 1) is set
y1 + 1 is natural V11() ext-real real V106() V107() V108() V109() V110() V111() bounded_below Element of NAT
d1 is natural V11() ext-real real V106() V107() V108() V109() V110() V111() bounded_below Element of NAT
y . ((len y) - y1) is set
[(y . ((len y) - y1)),(y . (((len y) - y1) + 1))] is set
{(y . ((len y) - y1)),(y . (((len y) - y1) + 1))} is non empty finite set
{(y . ((len y) - y1))} is non empty finite set
{{(y . ((len y) - y1)),(y . (((len y) - y1) + 1))},{(y . ((len y) - y1))}} is non empty finite V48() set
(len y) - (y1 + 1) is V11() ext-real real set
((len y) - (y1 + 1)) + 1 is V11() ext-real real set
y . (((len y) - (y1 + 1)) + 1) is set
[(y . (((len y) - y1) + 1)),(y . (((len y) - (y1 + 1)) + 1))] is set
{(y . (((len y) - y1) + 1)),(y . (((len y) - (y1 + 1)) + 1))} is non empty finite set
{(y . (((len y) - y1) + 1))} is non empty finite set
{{(y . (((len y) - y1) + 1)),(y . (((len y) - (y1 + 1)) + 1))},{(y . (((len y) - y1) + 1))}} is non empty finite V48() set
x1 . (y1 + 1) is set
[(x1 . y1),(x1 . (y1 + 1))] is set
{(x1 . y1),(x1 . (y1 + 1))} is non empty finite set
{(x1 . y1)} is non empty finite set
{{(x1 . y1),(x1 . (y1 + 1))},{(x1 . y1)}} is non empty finite V48() set
x1 . (len x1) is set
x1 . (len y) is set
x1 . 1 is set
[x,R] is set
{x,R} is non empty finite set
{x} is non empty finite set
{{x,R},{x}} is non empty finite V48() set
a is set
[:a,a:] is set
bool [:a,a:] is non empty set
M is Relation-like a -defined a -valued Element of bool [:a,a:]
M [*] is Relation-like set
R is set
x is set
y is set
[R,x] is set
{R,x} is non empty finite set
{R} is non empty finite set
{{R,x},{R}} is non empty finite V48() set
[x,y] is set
{x,y} is non empty finite set
{x} is non empty finite set
{{x,y},{x}} is non empty finite V48() set
[R,y] is set
{R,y} is non empty finite set
{{R,y},{R}} is non empty finite V48() set
a is non empty set
[:a,a:] is non empty set
bool [:a,a:] is non empty set
M is Relation-like a -defined a -valued Element of bool [:a,a:]
M [*] is Relation-like a -defined a -valued Element of bool [:a,a:]
dom (M [*]) is Element of bool a
bool a is non empty set
field (M [*]) is set
a is non empty set
[:a,a:] is non empty set
bool [:a,a:] is non empty set
M is Relation-like a -defined a -valued Element of bool [:a,a:]
R is Relation-like a -defined a -valued Element of bool [:a,a:]
M [*] is Relation-like a -defined a -valued Element of bool [:a,a:]
R [*] is Relation-like a -defined a -valued Element of bool [:a,a:]
field M is set
field R is set
x is set
y is set
x1 is set
[y,x1] is set
{y,x1} is non empty finite set
{y} is non empty finite set
{{y,x1},{y}} is non empty finite V48() set
y1 is Relation-like Function-like FinSequence-like set
len y1 is natural V11() ext-real real V106() V107() V108() V109() V110() V111() bounded_below Element of NAT
y1 . 1 is set
y1 . (len y1) is set
d1 is natural V11() ext-real real set
y1 . d1 is set
d1 + 1 is natural V11() ext-real real V106() V107() V108() V109() V110() V111() bounded_below Element of NAT
y1 . (d1 + 1) is set
[(y1 . d1),(y1 . (d1 + 1))] is set
{(y1 . d1),(y1 . (d1 + 1))} is non empty finite set
{(y1 . d1)} is non empty finite set
{{(y1 . d1),(y1 . (d1 + 1))},{(y1 . d1)}} is non empty finite V48() set
a is non empty set
M is non empty with_non-empty_elements a_partition of a
{a} is non empty finite set
{{a}} is non empty finite V48() set
R is non empty with_non-empty_elements a_partition of a
a is non empty set
%I a is non empty with_non-empty_elements a_partition of a
id a is non empty Relation-like a -defined a -valued total Element of bool [:a,a:]
[:a,a:] is non empty set
bool [:a,a:] is non empty set
Class (id a) is non empty with_non-empty_elements a_partition of a
{a} is non empty finite set
M is set
a is non empty set
PARTITIONS a is set
bool (PARTITIONS a) is non empty set
{a} is non empty finite set
{{a}} is non empty finite V48() set
M is Element of bool (PARTITIONS a)
R is non empty with_non-empty_elements a_partition of a
x is non empty with_non-empty_elements a_partition of a
a is non empty set
{a} is non empty finite set
{{a}} is non empty finite V48() set
PARTITIONS a is set
bool (PARTITIONS a) is non empty set
M is Element of bool (PARTITIONS a)
R is non empty with_non-empty_elements a_partition of a
x is non empty with_non-empty_elements a_partition of a
a is non empty set
%I a is non empty with_non-empty_elements a_partition of a
id a is non empty Relation-like a -defined a -valued total Element of bool [:a,a:]
[:a,a:] is non empty set
bool [:a,a:] is non empty set
Class (id a) is non empty with_non-empty_elements a_partition of a
{(%I a)} is non empty finite set
PARTITIONS a is set
bool (PARTITIONS a) is non empty set
M is Element of bool (PARTITIONS a)
R is non empty with_non-empty_elements a_partition of a
x is non empty with_non-empty_elements a_partition of a
a is non empty set
PARTITIONS a is set
bool (PARTITIONS a) is non empty set
{a} is non empty finite set
%I a is non empty with_non-empty_elements a_partition of a
id a is non empty Relation-like a -defined a -valued total Element of bool [:a,a:]
[:a,a:] is non empty set
bool [:a,a:] is non empty set
Class (id a) is non empty with_non-empty_elements a_partition of a
{{a},(%I a)} is non empty finite set
M is Element of bool (PARTITIONS a)
R is non empty with_non-empty_elements a_partition of a
x is non empty with_non-empty_elements a_partition of a
a is non empty set
PARTITIONS a is set
bool (PARTITIONS a) is non empty set
{a} is non empty finite set
%I a is non empty with_non-empty_elements a_partition of a
id a is non empty Relation-like a -defined a -valued total Element of bool [:a,a:]
[:a,a:] is non empty set
bool [:a,a:] is non empty set
Class (id a) is non empty with_non-empty_elements a_partition of a
{{a},(%I a)} is non empty finite set
M is Element of bool (PARTITIONS a)
a is non empty set
PARTITIONS a is set
bool (PARTITIONS a) is non empty set
{a} is non empty finite set
%I a is non empty with_non-empty_elements a_partition of a
id a is non empty Relation-like a -defined a -valued total Element of bool [:a,a:]
[:a,a:] is non empty set
bool [:a,a:] is non empty set
Class (id a) is non empty with_non-empty_elements a_partition of a
{{a},(%I a)} is non empty finite set
M is Element of bool (PARTITIONS a)
a is non empty set
[:a,a:] is non empty set
[:[:a,a:],REAL:] is non empty set
bool [:[:a,a:],REAL:] is non empty set
bool [:a,a:] is non empty set
M is Relation-like [:a,a:] -defined REAL -valued Function-like Element of bool [:[:a,a:],REAL:]
R is V11() ext-real real set
x is Relation-like a -defined a -valued Element of bool [:a,a:]
y is Element of a
x1 is Element of a
[y,x1] is set
{y,x1} is non empty finite set
{y} is non empty finite set
{{y,x1},{y}} is non empty finite V48() set
M . (y,x1) is V11() ext-real real Element of REAL
M . [y,x1] is set
y1 is Element of a
d1 is Element of a
M . (y1,d1) is V11() ext-real real Element of REAL
[y1,d1] is set
{y1,d1} is non empty finite set
{y1} is non empty finite set
{{y1,d1},{y1}} is non empty finite V48() set
M . [y1,d1] is set
x is Relation-like a -defined a -valued Element of bool [:a,a:]
y is Relation-like a -defined a -valued Element of bool [:a,a:]
x1 is set
y1 is set
[x1,y1] is set
{x1,y1} is non empty finite set
{x1} is non empty finite set
{{x1,y1},{x1}} is non empty finite V48() set
d1 is Element of a
y is Element of a
M . (d1,y) is V11() ext-real real Element of REAL
[d1,y] is set
{d1,y} is non empty finite set
{d1} is non empty finite set
{{d1,y},{d1}} is non empty finite V48() set
M . [d1,y] is set
x1 is set
y1 is set
[x1,y1] is set
{x1,y1} is non empty finite set
{x1} is non empty finite set
{{x1,y1},{x1}} is non empty finite V48() set
d1 is Element of a
y is Element of a
M . (d1,y) is V11() ext-real real Element of REAL
[d1,y] is set
{d1,y} is non empty finite set
{d1} is non empty finite set
{{d1,y},{d1}} is non empty finite V48() set
M . [d1,y] is set
a is non empty set
[:a,a:] is non empty set
[:[:a,a:],REAL:] is non empty set
bool [:[:a,a:],REAL:] is non empty set
M is Relation-like [:a,a:] -defined REAL -valued Function-like Element of bool [:[:a,a:],REAL:]
R is V11() ext-real real set
(a,M,R) is Relation-like a -defined a -valued Element of bool [:a,a:]
bool [:a,a:] is non empty set
x is set
y is Element of a
M . (y,y) is V11() ext-real real Element of REAL
[y,y] is set
{y,y} is non empty finite set
{y} is non empty finite set
{{y,y},{y}} is non empty finite V48() set
M . [y,y] is set
[x,x] is set
{x,x} is non empty finite set
{x} is non empty finite set
{{x,x},{x}} is non empty finite V48() set
a is non empty set
[:a,a:] is non empty set
[:[:a,a:],REAL:] is non empty set
bool [:[:a,a:],REAL:] is non empty set
M is Relation-like [:a,a:] -defined REAL -valued Function-like Element of bool [:[:a,a:],REAL:]
R is V11() ext-real real set
(a,M,R) is Relation-like a -defined a -valued Element of bool [:a,a:]
bool [:a,a:] is non empty set
x is set
y is set
[x,y] is set
{x,y} is non empty finite set
{x} is non empty finite set
{{x,y},{x}} is non empty finite V48() set
x1 is Element of a
y1 is Element of a
M . (x1,y1) is V11() ext-real real Element of REAL
[x1,y1] is set
{x1,y1} is non empty finite set
{x1} is non empty finite set
{{x1,y1},{x1}} is non empty finite V48() set
M . [x1,y1] is set
M . (y1,x1) is V11() ext-real real Element of REAL
[y1,x1] is set
{y1,x1} is non empty finite set
{y1} is non empty finite set
{{y1,x1},{y1}} is non empty finite V48() set
M . [y1,x1] is set
[y,x] is set
{y,x} is non empty finite set
{y} is non empty finite set
{{y,x},{y}} is non empty finite V48() set
a is non empty set
[:a,a:] is non empty set
[:[:a,a:],REAL:] is non empty set
bool [:[:a,a:],REAL:] is non empty set
bool [:a,a:] is non empty set
M is Relation-like [:a,a:] -defined REAL -valued Function-like Element of bool [:[:a,a:],REAL:]
R is V11() ext-real real set
(a,M,R) is Relation-like a -defined a -valued Element of bool [:a,a:]
dom (a,M,R) is Element of bool a
bool a is non empty set
field (a,M,R) is set
rng (a,M,R) is Element of bool a
a \/ (rng (a,M,R)) is non empty set
a is non empty set
[:a,a:] is non empty set
[:[:a,a:],REAL:] is non empty set
bool [:[:a,a:],REAL:] is non empty set
M is Relation-like [:a,a:] -defined REAL -valued Function-like Element of bool [:[:a,a:],REAL:]
R is V11() ext-real real set
x is V11() ext-real real set
(a,M,R) is Relation-like a -defined a -valued Element of bool [:a,a:]
bool [:a,a:] is non empty set
(a,M,x) is Relation-like a -defined a -valued Element of bool [:a,a:]
y is set
x1 is set
y1 is set
[x1,y1] is set
{x1,y1} is non empty finite set
{x1} is non empty finite set
{{x1,y1},{x1}} is non empty finite V48() set
d1 is Element of a
y is Element of a
M . (d1,y) is V11() ext-real real Element of REAL
[d1,y] is set
{d1,y} is non empty finite set
{d1} is non empty finite set
{{d1,y},{d1}} is non empty finite V48() set
M . [d1,y] is set
a is set
[:a,a:] is set
[:[:a,a:],REAL:] is set
bool [:[:a,a:],REAL:] is non empty set
a is non empty set
[:a,a:] is non empty set
[:[:a,a:],REAL:] is non empty set
bool [:[:a,a:],REAL:] is non empty set
M is Relation-like [:a,a:] -defined REAL -valued Function-like Element of bool [:[:a,a:],REAL:]
(a,M,0) is Relation-like a -defined a -valued Element of bool [:a,a:]
bool [:a,a:] is non empty set
R is set
x is set
[R,x] is set
{R,x} is non empty finite set
{R} is non empty finite set
{{R,x},{R}} is non empty finite V48() set
y is Element of a
x1 is Element of a
M . (y,x1) is V11() ext-real real Element of REAL
[y,x1] is set
{y,x1} is non empty finite set
{y} is non empty finite set
{{y,x1},{y}} is non empty finite V48() set
M . [y,x1] is set
a is non empty set
[:a,a:] is non empty set
[:[:a,a:],REAL:] is non empty set
bool [:[:a,a:],REAL:] is non empty set
M is Relation-like [:a,a:] -defined REAL -valued Function-like Element of bool [:[:a,a:],REAL:]
(a,M,0) is Relation-like a -defined a -valued Element of bool [:a,a:]
bool [:a,a:] is non empty set
R is Element of a
[R,R] is set
{R,R} is non empty finite set
{R} is non empty finite set
{{R,R},{R}} is non empty finite V48() set
M . (R,R) is V11() ext-real real Element of REAL
M . [R,R] is set
a is non empty set
[:a,a:] is non empty set
[:[:a,a:],REAL:] is non empty set
bool [:[:a,a:],REAL:] is non empty set
bool [:a,a:] is non empty set
M is Relation-like [:a,a:] -defined REAL -valued Function-like Element of bool [:[:a,a:],REAL:]
R is V11() ext-real real set
(a,M,R) is Relation-like a -defined a -valued Element of bool [:a,a:]
(a,M,R) [*] is Relation-like a -defined a -valued Element of bool [:a,a:]
x is set
y is set
[x,y] is set
{x,y} is non empty finite set
{x} is non empty finite set
{{x,y},{x}} is non empty finite V48() set
x1 is Element of a
y1 is Element of a
M . (x1,y1) is V11() ext-real real Element of REAL
[x1,y1] is set
{x1,y1} is non empty finite set
{x1} is non empty finite set
{{x1,y1},{x1}} is non empty finite V48() set
M . [x1,y1] is set
M . (y1,x1) is V11() ext-real real Element of REAL
[y1,x1] is set
{y1,x1} is non empty finite set
{y1} is non empty finite set
{{y1,x1},{y1}} is non empty finite V48() set
M . [y1,x1] is set
[y,x] is set
{y,x} is non empty finite set
{y} is non empty finite set
{{y,x},{y}} is non empty finite V48() set
a is set
M is non empty set
[:M,M:] is non empty set
[:[:M,M:],REAL:] is non empty set
bool [:[:M,M:],REAL:] is non empty set
bool [:M,M:] is non empty set
R is V11() ext-real non negative real set
x is V11() ext-real non negative real set
y is Relation-like [:M,M:] -defined REAL -valued Function-like Element of bool [:[:M,M:],REAL:]
(M,y,R) is Relation-like M -defined M -valued Element of bool [:M,M:]
(M,y,R) [*] is Relation-like M -defined M -valued Element of bool [:M,M:]
(M,y,x) is Relation-like M -defined M -valued Element of bool [:M,M:]
(M,y,x) [*] is Relation-like M -defined M -valued Element of bool [:M,M:]
x1 is Relation-like M -defined M -valued total symmetric transitive Element of bool [:M,M:]
y1 is Relation-like M -defined M -valued total symmetric transitive Element of bool [:M,M:]
Class (x1,a) is Element of bool M
bool M is non empty set
Class (y1,a) is Element of bool M
d1 is set
[d1,a] is set
{d1,a} is non empty finite set
{d1} is non empty finite set
{{d1,a},{d1}} is non empty finite V48() set
a is non empty set
[:a,a:] is non empty set
[:[:a,a:],REAL:] is non empty set
bool [:[:a,a:],REAL:] is non empty set
M is Relation-like [:a,a:] -defined REAL -valued Function-like Element of bool [:[:a,a:],REAL:]
(a,M,0) is Relation-like a -defined a -valued Element of bool [:a,a:]
bool [:a,a:] is non empty set
(a,M,0) [*] is Relation-like a -defined a -valued Element of bool [:a,a:]
R is set
x is set
y is set
[x,y] is set
{x,y} is non empty finite set
{x} is non empty finite set
{{x,y},{x}} is non empty finite V48() set
x1 is Relation-like Function-like FinSequence-like RedSequence of (a,M,0)
x1 . 1 is set
len x1 is natural V11() ext-real real V106() V107() V108() V109() V110() V111() bounded_below Element of NAT
x1 . (len x1) is set
y1 is natural V11() ext-real real set
dom x1 is V106() V107() V108() V109() V110() V111() bounded_below Element of bool NAT
y1 + 1 is natural V11() ext-real real V106() V107() V108() V109() V110() V111() bounded_below Element of NAT
x1 . y1 is set
x1 . (y1 + 1) is set
[(x1 . y1),(x1 . (y1 + 1))] is set
{(x1 . y1),(x1 . (y1 + 1))} is non empty finite set
{(x1 . y1)} is non empty finite set
{{(x1 . y1),(x1 . (y1 + 1))},{(x1 . y1)}} is non empty finite V48() set
0 + 1 is non empty natural V11() ext-real positive non negative real V106() V107() V108() V109() V110() V111() left_end bounded_below Element of NAT
a is non empty set
[:a,a:] is non empty set
[:[:a,a:],REAL:] is non empty set
bool [:[:a,a:],REAL:] is non empty set
bool [:a,a:] is non empty set
id a is non empty Relation-like set
M is Relation-like [:a,a:] -defined REAL -valued Function-like Element of bool [:[:a,a:],REAL:]
(a,M,0) is Relation-like a -defined a -valued Element of bool [:a,a:]
(a,M,0) [*] is Relation-like a -defined a -valued Element of bool [:a,a:]
R is Relation-like a -defined a -valued total symmetric transitive Element of bool [:a,a:]
x is set
y is set
[x,y] is set
{x,y} is non empty finite set
{x} is non empty finite set
{{x,y},{x}} is non empty finite V48() set
x is set
y is set
[x,y] is set
{x,y} is non empty finite set
{x} is non empty finite set
{{x,y},{x}} is non empty finite V48() set
a is non empty set
[:a,a:] is non empty set
[:[:a,a:],REAL:] is non empty set
bool [:[:a,a:],REAL:] is non empty set
bool [:a,a:] is non empty set
R is Relation-like a -defined a -valued total symmetric transitive Element of bool [:a,a:]
M is Relation-like [:a,a:] -defined REAL -valued Function-like Element of bool [:[:a,a:],REAL:]
(a,M,0) is Relation-like a -defined a -valued Element of bool [:a,a:]
(a,M,0) [*] is Relation-like a -defined a -valued Element of bool [:a,a:]
Class R is non empty with_non-empty_elements a_partition of a
%I a is non empty with_non-empty_elements a_partition of a
id a is non empty Relation-like a -defined a -valued total Element of bool [:a,a:]
Class (id a) is non empty with_non-empty_elements a_partition of a
a is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL
[:a,a:] is non empty finite set
[:[:a,a:],REAL:] is non empty set
bool [:[:a,a:],REAL:] is non empty set
M is Relation-like [:a,a:] -defined REAL -valued Function-like V29([:a,a:], REAL ) finite Element of bool [:[:a,a:],REAL:]
rng M is finite V106() V107() V108() bounded_below bounded_above real-bounded Element of bool REAL
R is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL
max R is V11() ext-real real set
x is V11() ext-real real set
y is V11() ext-real real Element of a
x1 is V11() ext-real real Element of a
[y,x1] is set
{y,x1} is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded set
{y} is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded set
{{y,x1},{y}} is non empty finite V48() set
M . [y,x1] is set
M . (y,x1) is V11() ext-real real Element of REAL
dom M is Relation-like a -defined a -valued finite Element of bool [:a,a:]
bool [:a,a:] is non empty finite V48() set
y1 is V11() ext-real real set
y is V11() ext-real real Element of a
x1 is V11() ext-real real Element of a
M . (y,x1) is V11() ext-real real Element of REAL
[y,x1] is set
{y,x1} is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded set
{y} is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded set
{{y,x1},{y}} is non empty finite V48() set
M . [y,x1] is set
a is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL
[:a,a:] is non empty finite set
[:[:a,a:],REAL:] is non empty set
bool [:[:a,a:],REAL:] is non empty set
bool [:a,a:] is non empty finite V48() set
{a} is non empty finite V48() set
M is Relation-like [:a,a:] -defined REAL -valued Function-like V29([:a,a:], REAL ) finite Element of bool [:[:a,a:],REAL:]
rng M is finite V106() V107() V108() bounded_below bounded_above real-bounded Element of bool REAL
R is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL
max R is V11() ext-real real set
x is V11() ext-real real set
(a,M,x) is Relation-like a -defined a -valued finite Element of bool [:a,a:]
(a,M,x) [*] is Relation-like a -defined a -valued finite Element of bool [:a,a:]
y is Relation-like a -defined a -valued total symmetric transitive finite Element of bool [:a,a:]
x1 is set
Class (y,x1) is finite V106() V107() V108() bounded_below bounded_above real-bounded Element of bool a
bool a is non empty finite V48() set
d1 is set
y is V11() ext-real real Element of a
y1 is V11() ext-real real Element of a
M . (y,y1) is V11() ext-real real Element of REAL
[y,y1] is set
{y,y1} is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded set
{y} is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded set
{{y,y1},{y}} is non empty finite V48() set
M . [y,y1] is set
[d1,x1] is set
{d1,x1} is non empty finite set
{d1} is non empty finite set
{{d1,x1},{d1}} is non empty finite V48() set
x1 is set
y1 is set
Class (y,y1) is finite V106() V107() V108() bounded_below bounded_above real-bounded Element of bool a
bool a is non empty finite V48() set
Class y is non empty with_non-empty_elements finite V48() a_partition of a
x1 is set
y1 is set
Class (y,y1) is finite V106() V107() V108() bounded_below bounded_above real-bounded Element of bool a
y is Relation-like a -defined a -valued total symmetric transitive finite Element of bool [:a,a:]
Class y is non empty with_non-empty_elements finite V48() a_partition of a
a is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL
[:a,a:] is non empty finite set
[:[:a,a:],REAL:] is non empty set
bool [:[:a,a:],REAL:] is non empty set
M is Relation-like [:a,a:] -defined REAL -valued Function-like V29([:a,a:], REAL ) finite Element of bool [:[:a,a:],REAL:]
rng M is finite V106() V107() V108() bounded_below bounded_above real-bounded Element of bool REAL
R is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL
max R is V11() ext-real real set
x is V11() ext-real real set
(a,M,x) is Relation-like a -defined a -valued finite Element of bool [:a,a:]
bool [:a,a:] is non empty finite V48() set
(a,M,x) [*] is Relation-like a -defined a -valued finite Element of bool [:a,a:]
y is set
x1 is set
y1 is set
[x1,y1] is set
{x1,y1} is non empty finite set
{x1} is non empty finite set
{{x1,y1},{x1}} is non empty finite V48() set
d1 is V11() ext-real real Element of a
y is V11() ext-real real Element of a
M . (d1,y) is V11() ext-real real Element of REAL
[d1,y] is set
{d1,y} is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded set
{d1} is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded set
{{d1,y},{d1}} is non empty finite V48() set
M . [d1,y] is set
a is non empty set
[:a,a:] is non empty set
[:[:a,a:],REAL:] is non empty set
bool [:[:a,a:],REAL:] is non empty set
PARTITIONS a is set
bool (PARTITIONS a) is non empty set
bool [:a,a:] is non empty set
M is Relation-like [:a,a:] -defined REAL -valued Function-like Element of bool [:[:a,a:],REAL:]
R is set
x is set
x is Element of bool (PARTITIONS a)
y is set
y1 is Relation-like a -defined a -valued total symmetric transitive Element of bool [:a,a:]
x1 is V11() ext-real non negative real set
(a,M,x1) is Relation-like a -defined a -valued Element of bool [:a,a:]
(a,M,x1) [*] is Relation-like a -defined a -valued Element of bool [:a,a:]
Class y1 is non empty with_non-empty_elements a_partition of a
R is Element of bool (PARTITIONS a)
x is Element of bool (PARTITIONS a)
a is non empty set
[:a,a:] is non empty set
[:[:a,a:],REAL:] is non empty set
bool [:[:a,a:],REAL:] is non empty set
M is Relation-like [:a,a:] -defined REAL -valued Function-like Element of bool [:[:a,a:],REAL:]
(a,M) is Element of bool (PARTITIONS a)
PARTITIONS a is set
bool (PARTITIONS a) is non empty set
R is V11() ext-real non negative real set
(a,M,R) is Relation-like a -defined a -valued Element of bool [:a,a:]
bool [:a,a:] is non empty set
(a,M,R) [*] is Relation-like a -defined a -valued Element of bool [:a,a:]
x is Relation-like a -defined a -valued total symmetric transitive Element of bool [:a,a:]
Class x is non empty with_non-empty_elements a_partition of a
y is set
a is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL
[:a,a:] is non empty finite set
[:[:a,a:],REAL:] is non empty set
bool [:[:a,a:],REAL:] is non empty set
{a} is non empty finite V48() set
M is Relation-like [:a,a:] -defined REAL -valued Function-like V29([:a,a:], REAL ) finite Element of bool [:[:a,a:],REAL:]
(a,M) is Element of bool (PARTITIONS a)
PARTITIONS a is set
bool (PARTITIONS a) is non empty set
dom M is Relation-like a -defined a -valued finite Element of bool [:a,a:]
bool [:a,a:] is non empty finite V48() set
rng M is finite V106() V107() V108() bounded_below bounded_above real-bounded Element of bool REAL
R is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL
max R is V11() ext-real real set
the V11() ext-real real Element of a is V11() ext-real real Element of a
x is V11() ext-real real set
M . ( the V11() ext-real real Element of a, the V11() ext-real real Element of a) is V11() ext-real real Element of REAL
[ the V11() ext-real real Element of a, the V11() ext-real real Element of a] is set
{ the V11() ext-real real Element of a, the V11() ext-real real Element of a} is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded set
{ the V11() ext-real real Element of a} is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded set
{{ the V11() ext-real real Element of a, the V11() ext-real real Element of a},{ the V11() ext-real real Element of a}} is non empty finite V48() set
M . [ the V11() ext-real real Element of a, the V11() ext-real real Element of a] is set
x1 is set
y1 is V11() ext-real real Element of a
M . (y1,y1) is V11() ext-real real Element of REAL
[y1,y1] is set
{y1,y1} is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded set
{y1} is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded set
{{y1,y1},{y1}} is non empty finite V48() set
M . [y1,y1] is set
[x1,x1] is set
{x1,x1} is non empty finite set
{x1} is non empty finite set
{{x1,x1},{x1}} is non empty finite V48() set
(a,M,x) is Relation-like a -defined a -valued finite Element of bool [:a,a:]
y is V11() ext-real non negative real set
(a,M,y) is Relation-like a -defined a -valued finite Element of bool [:a,a:]
(a,M,y) [*] is Relation-like a -defined a -valued finite Element of bool [:a,a:]
x1 is Relation-like a -defined a -valued total symmetric transitive finite Element of bool [:a,a:]
Class x1 is non empty with_non-empty_elements finite V48() a_partition of a
a is non empty set
[:a,a:] is non empty set
[:[:a,a:],REAL:] is non empty set
bool [:[:a,a:],REAL:] is non empty set
M is Relation-like [:a,a:] -defined REAL -valued Function-like Element of bool [:[:a,a:],REAL:]
(a,M) is Element of bool (PARTITIONS a)
PARTITIONS a is set
bool (PARTITIONS a) is non empty set
R is non empty with_non-empty_elements a_partition of a
x is non empty with_non-empty_elements a_partition of a
bool [:a,a:] is non empty set
x1 is Relation-like a -defined a -valued total symmetric transitive Element of bool [:a,a:]
y is V11() ext-real non negative real set
(a,M,y) is Relation-like a -defined a -valued Element of bool [:a,a:]
(a,M,y) [*] is Relation-like a -defined a -valued Element of bool [:a,a:]
Class x1 is non empty with_non-empty_elements a_partition of a
d1 is Relation-like a -defined a -valued total symmetric transitive Element of bool [:a,a:]
y1 is V11() ext-real non negative real set
(a,M,y1) is Relation-like a -defined a -valued Element of bool [:a,a:]
(a,M,y1) [*] is Relation-like a -defined a -valued Element of bool [:a,a:]
Class d1 is non empty with_non-empty_elements a_partition of a
y is set
c is set
Class (x1,c) is Element of bool a
bool a is non empty set
Class (d1,c) is Element of bool a
x is set
x is set
y is set
c is set
Class (d1,c) is Element of bool a
bool a is non empty set
Class (x1,c) is Element of bool a
x is set
x is set
a is non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL
[:a,a:] is non empty finite set
[:[:a,a:],REAL:] is non empty set
bool [:[:a,a:],REAL:] is non empty set
%I a is non empty with_non-empty_elements finite V48() a_partition of a
id a is non empty Relation-like a -defined a -valued total finite Element of bool [:a,a:]
bool [:a,a:] is non empty finite V48() set
Class (id a) is non empty with_non-empty_elements finite V48() a_partition of a
M is Relation-like [:a,a:] -defined REAL -valued Function-like V29([:a,a:], REAL ) finite Element of bool [:[:a,a:],REAL:]
(a,M) is Element of bool (PARTITIONS a)
PARTITIONS a is set
bool (PARTITIONS a) is non empty set
{a} is non empty finite V48() set
a is MetrStruct
the carrier of a is set
a is non empty MetrStruct
the carrier of a is non empty set
[: the carrier of a, the carrier of a:] is non empty set
bool [: the carrier of a, the carrier of a:] is non empty set
M is V11() ext-real real set
R is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]
x is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]
y is Element of the carrier of a
x1 is Element of the carrier of a
[y,x1] is set
{y,x1} is non empty finite set
{y} is non empty finite set
{{y,x1},{y}} is non empty finite V48() set
y1 is Element of the carrier of a
d1 is Element of the carrier of a
[y1,d1] is set
{y1,d1} is non empty finite set
{y1} is non empty finite set
{{y1,d1},{y1}} is non empty finite V48() set
R is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]
x is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]
y is set
x1 is set
[y,x1] is set
{y,x1} is non empty finite set
{y} is non empty finite set
{{y,x1},{y}} is non empty finite V48() set
y1 is Element of the carrier of a
d1 is Element of the carrier of a
y is set
x1 is set
[y,x1] is set
{y,x1} is non empty finite set
{y} is non empty finite set
{{y,x1},{y}} is non empty finite V48() set
y1 is Element of the carrier of a
d1 is Element of the carrier of a
a is non empty MetrStruct
the carrier of a is non empty set
the distance of a is Relation-like [: the carrier of a, the carrier of a:] -defined REAL -valued Function-like V29([: the carrier of a, the carrier of a:], REAL ) Element of bool [:[: the carrier of a, the carrier of a:],REAL:]
[: the carrier of a, the carrier of a:] is non empty set
[:[: the carrier of a, the carrier of a:],REAL:] is non empty set
bool [:[: the carrier of a, the carrier of a:],REAL:] is non empty set
M is V11() ext-real real set
(a,M) is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]
bool [: the carrier of a, the carrier of a:] is non empty set
( the carrier of a, the distance of a,M) is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]
R is set
x is set
y is set
[x,y] is set
{x,y} is non empty finite set
{x} is non empty finite set
{{x,y},{x}} is non empty finite V48() set
x1 is Element of the carrier of a
y1 is Element of the carrier of a
dist (x1,y1) is V11() ext-real real Element of REAL
the distance of a . (x1,y1) is V11() ext-real real Element of REAL
[x1,y1] is set
{x1,y1} is non empty finite set
{x1} is non empty finite set
{{x1,y1},{x1}} is non empty finite V48() set
the distance of a . [x1,y1] is set
R is set
x is set
y is set
[x,y] is set
{x,y} is non empty finite set
{x} is non empty finite set
{{x,y},{x}} is non empty finite V48() set
x1 is Element of the carrier of a
y1 is Element of the carrier of a
the distance of a . (x1,y1) is V11() ext-real real Element of REAL
[x1,y1] is set
{x1,y1} is non empty finite set
{x1} is non empty finite set
{{x1,y1},{x1}} is non empty finite V48() set
the distance of a . [x1,y1] is set
dist (x1,y1) is V11() ext-real real Element of REAL
a is non empty Reflexive symmetric MetrStruct
the carrier of a is non empty set
[: the carrier of a, the carrier of a:] is non empty set
bool [: the carrier of a, the carrier of a:] is non empty set
M is V11() ext-real real set
(a,M) is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]
R is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]
the distance of a is Relation-like [: the carrier of a, the carrier of a:] -defined REAL -valued Function-like V29([: the carrier of a, the carrier of a:], REAL ) Element of bool [:[: the carrier of a, the carrier of a:],REAL:]
[:[: the carrier of a, the carrier of a:],REAL:] is non empty set
bool [:[: the carrier of a, the carrier of a:],REAL:] is non empty set
( the carrier of a, the distance of a,M) is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]
a is non empty Reflexive symmetric MetrStruct
the carrier of a is non empty set
PARTITIONS the carrier of a is set
bool (PARTITIONS the carrier of a) is non empty set
[: the carrier of a, the carrier of a:] is non empty set
bool [: the carrier of a, the carrier of a:] is non empty set
M is set
R is set
R is Element of bool (PARTITIONS the carrier of a)
x is set
x1 is Relation-like the carrier of a -defined the carrier of a -valued total symmetric transitive Element of bool [: the carrier of a, the carrier of a:]
y is V11() ext-real non negative real set
(a,y) is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]
(a,y) [*] is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]
Class x1 is non empty with_non-empty_elements a_partition of the carrier of a
M is Element of bool (PARTITIONS the carrier of a)
R is Element of bool (PARTITIONS the carrier of a)
a is non empty Reflexive symmetric MetrStruct
(a) is Element of bool (PARTITIONS the carrier of a)
the carrier of a is non empty set
PARTITIONS the carrier of a is set
bool (PARTITIONS the carrier of a) is non empty set
the distance of a is Relation-like [: the carrier of a, the carrier of a:] -defined REAL -valued Function-like V29([: the carrier of a, the carrier of a:], REAL ) Element of bool [:[: the carrier of a, the carrier of a:],REAL:]
[: the carrier of a, the carrier of a:] is non empty set
[:[: the carrier of a, the carrier of a:],REAL:] is non empty set
bool [:[: the carrier of a, the carrier of a:],REAL:] is non empty set
( the carrier of a, the distance of a) is Element of bool (PARTITIONS the carrier of a)
M is set
bool [: the carrier of a, the carrier of a:] is non empty set
x is Relation-like the carrier of a -defined the carrier of a -valued total symmetric transitive Element of bool [: the carrier of a, the carrier of a:]
R is V11() ext-real non negative real set
( the carrier of a, the distance of a,R) is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]
( the carrier of a, the distance of a,R) [*] is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]
Class x is non empty with_non-empty_elements a_partition of the carrier of a
y is Relation-like the carrier of a -defined the carrier of a -valued total symmetric transitive Element of bool [: the carrier of a, the carrier of a:]
(a,R) is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]
(a,R) [*] is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]
M is set
x is Relation-like the carrier of a -defined the carrier of a -valued total symmetric transitive Element of bool [: the carrier of a, the carrier of a:]
R is V11() ext-real non negative real set
(a,R) is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]
(a,R) [*] is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]
Class x is non empty with_non-empty_elements a_partition of the carrier of a
( the carrier of a, the distance of a,R) is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]
( the carrier of a, the distance of a,R) [*] is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]
a is non empty Reflexive discerning symmetric triangle MetrStruct
the carrier of a is non empty set
[: the carrier of a, the carrier of a:] is non empty set
bool [: the carrier of a, the carrier of a:] is non empty set
(a,0) is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]
(a,0) [*] is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]
%I the carrier of a is non empty with_non-empty_elements a_partition of the carrier of a
id the carrier of a is non empty Relation-like the carrier of a -defined the carrier of a -valued total Element of bool [: the carrier of a, the carrier of a:]
Class (id the carrier of a) is non empty with_non-empty_elements a_partition of the carrier of a
M is Element of the carrier of a
R is Element of the carrier of a
dist (M,R) is V11() ext-real real Element of REAL
the distance of a is Relation-like [: the carrier of a, the carrier of a:] -defined REAL -valued Function-like V29([: the carrier of a, the carrier of a:], REAL ) Element of bool [:[: the carrier of a, the carrier of a:],REAL:]
[:[: the carrier of a, the carrier of a:],REAL:] is non empty set
bool [:[: the carrier of a, the carrier of a:],REAL:] is non empty set
the distance of a . (M,R) is V11() ext-real real Element of REAL
[M,R] is set
{M,R} is non empty finite set
{M} is non empty finite set
{{M,R},{M}} is non empty finite V48() set
the distance of a . [M,R] is set
M is Relation-like the carrier of a -defined the carrier of a -valued total symmetric transitive Element of bool [: the carrier of a, the carrier of a:]
Class M is non empty with_non-empty_elements a_partition of the carrier of a
( the carrier of a, the distance of a,0) is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]
( the carrier of a, the distance of a,0) [*] is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]
a is V11() ext-real real set
M is non empty Reflexive symmetric bounded MetrStruct
[#] M is non empty non proper bounded Element of bool the carrier of M
the carrier of M is non empty set
bool the carrier of M is non empty set
diameter ([#] M) is V11() ext-real real Element of REAL
(M,a) is Relation-like the carrier of M -defined the carrier of M -valued Element of bool [: the carrier of M, the carrier of M:]
[: the carrier of M, the carrier of M:] is non empty set
bool [: the carrier of M, the carrier of M:] is non empty set
nabla the carrier of M is Relation-like the carrier of M -defined the carrier of M -valued total reflexive symmetric transitive Element of bool [: the carrier of M, the carrier of M:]
R is set
x is set
y is set
[x,y] is set
{x,y} is non empty finite set
{x} is non empty finite set
{{x,y},{x}} is non empty finite V48() set
x1 is Element of the carrier of M
y1 is Element of the carrier of M
dist (x1,y1) is V11() ext-real real Element of REAL
a is V11() ext-real real set
M is non empty Reflexive symmetric bounded MetrStruct
[#] M is non empty non proper bounded Element of bool the carrier of M
the carrier of M is non empty set
bool the carrier of M is non empty set
diameter ([#] M) is V11() ext-real real Element of REAL
(M,a) is Relation-like the carrier of M -defined the carrier of M -valued Element of bool [: the carrier of M, the carrier of M:]
[: the carrier of M, the carrier of M:] is non empty set
bool [: the carrier of M, the carrier of M:] is non empty set
(M,a) [*] is Relation-like the carrier of M -defined the carrier of M -valued Element of bool [: the carrier of M, the carrier of M:]
nabla the carrier of M is Relation-like the carrier of M -defined the carrier of M -valued total reflexive symmetric transitive Element of bool [: the carrier of M, the carrier of M:]
a is V11() ext-real real set
M is non empty Reflexive symmetric bounded MetrStruct
[#] M is non empty non proper bounded Element of bool the carrier of M
the carrier of M is non empty set
bool the carrier of M is non empty set
diameter ([#] M) is V11() ext-real real Element of REAL
(M,a) is Relation-like the carrier of M -defined the carrier of M -valued Element of bool [: the carrier of M, the carrier of M:]
[: the carrier of M, the carrier of M:] is non empty set
bool [: the carrier of M, the carrier of M:] is non empty set
(M,a) [*] is Relation-like the carrier of M -defined the carrier of M -valued Element of bool [: the carrier of M, the carrier of M:]
nabla the carrier of M is Relation-like the carrier of M -defined the carrier of M -valued total reflexive symmetric transitive Element of bool [: the carrier of M, the carrier of M:]
a is non empty Reflexive symmetric bounded MetrStruct
the carrier of a is non empty set
[: the carrier of a, the carrier of a:] is non empty set
bool [: the carrier of a, the carrier of a:] is non empty set
[#] a is non empty non proper bounded Element of bool the carrier of a
bool the carrier of a is non empty set
diameter ([#] a) is V11() ext-real real Element of REAL
{ the carrier of a} is non empty finite set
M is Relation-like the carrier of a -defined the carrier of a -valued total symmetric transitive Element of bool [: the carrier of a, the carrier of a:]
Class M is non empty with_non-empty_elements a_partition of the carrier of a
R is V11() ext-real non negative real set
(a,R) is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]
(a,R) [*] is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]
nabla the carrier of a is Relation-like the carrier of a -defined the carrier of a -valued total reflexive symmetric transitive Element of bool [: the carrier of a, the carrier of a:]
Class (nabla the carrier of a) is non empty with_non-empty_elements a_partition of the carrier of a
a is non empty Reflexive symmetric triangle MetrStruct
the carrier of a is non empty set
bool the carrier of a is non empty set
M is non empty bounded Element of bool the carrier of a
diameter M is V11() ext-real real Element of REAL
a is non empty Reflexive discerning symmetric triangle bounded MetrStruct
the carrier of a is non empty set
{ the carrier of a} is non empty finite set
(a) is Element of bool (PARTITIONS the carrier of a)
PARTITIONS the carrier of a is set
bool (PARTITIONS the carrier of a) is non empty set
[#] a is non empty non proper bounded Element of bool the carrier of a
bool the carrier of a is non empty set
diameter ([#] a) is V11() ext-real non negative real Element of REAL
the distance of a is Relation-like [: the carrier of a, the carrier of a:] -defined REAL -valued Function-like V29([: the carrier of a, the carrier of a:], REAL ) Element of bool [:[: the carrier of a, the carrier of a:],REAL:]
[: the carrier of a, the carrier of a:] is non empty set
[:[: the carrier of a, the carrier of a:],REAL:] is non empty set
bool [:[: the carrier of a, the carrier of a:],REAL:] is non empty set
( the carrier of a, the distance of a,(diameter ([#] a))) is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]
bool [: the carrier of a, the carrier of a:] is non empty set
(a,(diameter ([#] a))) is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]
(a,(diameter ([#] a))) [*] is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]
R is Relation-like the carrier of a -defined the carrier of a -valued total symmetric transitive Element of bool [: the carrier of a, the carrier of a:]
Class R is non empty with_non-empty_elements a_partition of the carrier of a
a is non empty Reflexive symmetric MetrStruct
(a) is Element of bool (PARTITIONS the carrier of a)
the carrier of a is non empty set
PARTITIONS the carrier of a is set
bool (PARTITIONS the carrier of a) is non empty set
the distance of a is Relation-like [: the carrier of a, the carrier of a:] -defined REAL -valued Function-like V29([: the carrier of a, the carrier of a:], REAL ) Element of bool [:[: the carrier of a, the carrier of a:],REAL:]
[: the carrier of a, the carrier of a:] is non empty set
[:[: the carrier of a, the carrier of a:],REAL:] is non empty set
bool [:[: the carrier of a, the carrier of a:],REAL:] is non empty set
( the carrier of a, the distance of a) is Element of bool (PARTITIONS the carrier of a)
M is non empty Reflexive discerning symmetric triangle bounded MetrStruct
(M) is Element of bool (PARTITIONS the carrier of M)
the carrier of M is non empty set
PARTITIONS the carrier of M is set
bool (PARTITIONS the carrier of M) is non empty set
the distance of M is Relation-like [: the carrier of M, the carrier of M:] -defined REAL -valued Function-like V29([: the carrier of M, the carrier of M:], REAL ) Element of bool [:[: the carrier of M, the carrier of M:],REAL:]
[: the carrier of M, the carrier of M:] is non empty set
[:[: the carrier of M, the carrier of M:],REAL:] is non empty set
bool [:[: the carrier of M, the carrier of M:],REAL:] is non empty set
a is V11() ext-real non negative real set
( the carrier of M, the distance of M,a) is Relation-like the carrier of M -defined the carrier of M -valued Element of bool [: the carrier of M, the carrier of M:]
bool [: the carrier of M, the carrier of M:] is non empty set
(M,a) is Relation-like the carrier of M -defined the carrier of M -valued Element of bool [: the carrier of M, the carrier of M:]
(M,a) [*] is Relation-like the carrier of M -defined the carrier of M -valued Element of bool [: the carrier of M, the carrier of M:]
R is Relation-like the carrier of M -defined the carrier of M -valued total symmetric transitive Element of bool [: the carrier of M, the carrier of M:]
Class R is non empty with_non-empty_elements a_partition of the carrier of M
%I the carrier of M is non empty with_non-empty_elements a_partition of the carrier of M
id the carrier of M is non empty Relation-like the carrier of M -defined the carrier of M -valued total Element of bool [: the carrier of M, the carrier of M:]
Class (id the carrier of M) is non empty with_non-empty_elements a_partition of the carrier of M
{ the carrier of M} is non empty finite set