:: LFUZZY_1 semantic presentation

REAL is non empty V43() V44() V45() V49() V52() set
NAT is V43() V44() V45() V46() V47() V48() V49() Element of bool REAL
bool REAL is non empty set
COMPLEX is non empty V43() V49() V52() set
{} is empty Relation-like non-empty empty-yielding V43() V44() V45() V46() V47() V48() V49() set
the empty Relation-like non-empty empty-yielding V43() V44() V45() V46() V47() V48() V49() set is empty Relation-like non-empty empty-yielding V43() V44() V45() V46() V47() V48() V49() set
1 is non empty ordinal natural V24() ext-real positive non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT
{{},1} is non empty set
omega is V43() V44() V45() V46() V47() V48() V49() set
bool omega is non empty set
bool NAT is non empty set
RAT is non empty V43() V44() V45() V46() V49() V52() set
INT is non empty V43() V44() V45() V46() V47() V49() V52() set
[:REAL,REAL:] is non empty Relation-like set
bool [:REAL,REAL:] is non empty set
K336() is non empty V92() L8()
the carrier of K336() is non empty set
K341() is non empty V92() V114() V115() V116() V118() V148() V149() V150() V151() V152() V153() L8()
K342() is non empty V92() V116() V118() V151() V152() V153() M13(K341())
K343() is non empty V92() V114() V116() V118() V151() V152() V153() V154() M16(K341(),K342())
K345() is non empty V92() V114() V116() V118() L8()
K346() is non empty V92() V114() V116() V118() V154() M13(K345())
0 is empty Relation-like non-empty empty-yielding ordinal natural V24() ext-real non positive non negative real V43() V44() V45() V46() V47() V48() V49() V50() V51() Element of NAT
[.0,1.] is non empty V43() V44() V45() Element of bool REAL
RealPoset [.0,1.] is non empty V183() reflexive transitive antisymmetric V191() with_suprema with_infima complete connected distributive Heyting real V278() L14()
the carrier of (RealPoset [.0,1.]) is non empty set
[:COMPLEX,COMPLEX:] is non empty Relation-like set
bool [:COMPLEX,COMPLEX:] is non empty set
[:COMPLEX,REAL:] is non empty Relation-like set
bool [:COMPLEX,REAL:] is non empty set
X is non empty set
[:X,REAL:] is non empty Relation-like set
bool [:X,REAL:] is non empty set
R is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
X is non empty set
R is non empty set
[:X,R:] is non empty Relation-like set
[:[:X,R:],REAL:] is non empty Relation-like set
bool [:[:X,R:],REAL:] is non empty set
S is non empty Relation-like [:X,R:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,R:],REAL:]
Q is non empty Relation-like [:X,R:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,R:],REAL:]
RP is Element of X
c is Element of R
S . (RP,c) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[RP,c] is set
{RP,c} is non empty set
{RP} is non empty set
{{RP,c},{RP}} is non empty set
S . [RP,c] is set
Q . (RP,c) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
Q . [RP,c] is set
dom S is non empty Relation-like X -defined R -valued Element of bool [:X,R:]
bool [:X,R:] is non empty set
[RP,c] is Element of [:X,R:]
dom S is non empty Relation-like X -defined R -valued Element of bool [:X,R:]
bool [:X,R:] is non empty set
RP is set
S . RP is V24() ext-real real Element of REAL
Q . RP is V24() ext-real real Element of REAL
c is set
t is set
[c,t] is set
{c,t} is non empty set
{c} is non empty set
{{c,t},{c}} is non empty set
n is Element of X
i is Element of R
S . (n,i) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[n,i] is set
{n,i} is non empty set
{n} is non empty set
{{n,i},{n}} is non empty set
S . [n,i] is set
Q . (n,i) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
Q . [n,i] is set
dom Q is non empty Relation-like X -defined R -valued Element of bool [:X,R:]
X is non empty set
[:X,REAL:] is non empty Relation-like set
bool [:X,REAL:] is non empty set
R is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
S is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
dom R is non empty Element of bool X
bool X is non empty set
Q is Element of X
R . Q is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
S . Q is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
dom S is non empty Element of bool X
X is non empty set
R is non empty set
[:X,R:] is non empty Relation-like set
[:[:X,R:],REAL:] is non empty Relation-like set
bool [:[:X,R:],REAL:] is non empty set
S is non empty Relation-like [:X,R:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,R:],REAL:]
Q is non empty Relation-like [:X,R:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,R:],REAL:]
dom S is non empty Relation-like X -defined R -valued Element of bool [:X,R:]
bool [:X,R:] is non empty set
RP is set
c is set
[RP,c] is set
{RP,c} is non empty set
{RP} is non empty set
{{RP,c},{RP}} is non empty set
S . (RP,c) is V24() ext-real real Element of REAL
S . [RP,c] is set
Q . (RP,c) is V24() ext-real real Element of REAL
Q . [RP,c] is set
t is Element of X
i is Element of R
S . (t,i) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[t,i] is set
{t,i} is non empty set
{t} is non empty set
{{t,i},{t}} is non empty set
S . [t,i] is set
Q . (t,i) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
Q . [t,i] is set
dom Q is non empty Relation-like X -defined R -valued Element of bool [:X,R:]
X is non empty set
[:X,REAL:] is non empty Relation-like set
bool [:X,REAL:] is non empty set
R is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
S is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
Q is Element of X
R . Q is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
S . Q is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
X is non empty set
[:X,REAL:] is non empty Relation-like set
bool [:X,REAL:] is non empty set
R is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
X is non empty set
[:X,REAL:] is non empty Relation-like set
bool [:X,REAL:] is non empty set
R is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
S is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
Q is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
RP is Element of X
R . RP is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
Q . RP is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
S . RP is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
X is non empty set
R is non empty set
[:X,R:] is non empty Relation-like set
[:[:X,R:],REAL:] is non empty Relation-like set
bool [:[:X,R:],REAL:] is non empty set
S is non empty set
[:R,S:] is non empty Relation-like set
[:[:R,S:],REAL:] is non empty Relation-like set
bool [:[:R,S:],REAL:] is non empty set
Q is non empty Relation-like [:X,R:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,R:],REAL:]
RP is non empty Relation-like [:X,R:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,R:],REAL:]
c is non empty Relation-like [:R,S:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:R,S:],REAL:]
t is non empty Relation-like [:R,S:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:R,S:],REAL:]
Q (#) c is non empty Relation-like [:X,S:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,S:],REAL:]
[:X,S:] is non empty Relation-like set
[:[:X,S:],REAL:] is non empty Relation-like set
bool [:[:X,S:],REAL:] is non empty set
RP (#) t is non empty Relation-like [:X,S:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,S:],REAL:]
i is Element of [:X,S:]
(Q (#) c) . i is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(RP (#) t) . i is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
n is set
j is set
[n,j] is set
{n,j} is non empty set
{n} is non empty set
{{n,j},{n}} is non empty set
f is set
[n,f] is set
{n,f} is non empty set
{{n,f},{n}} is non empty set
Q . [n,f] is V24() ext-real real Element of REAL
RP . [n,f] is V24() ext-real real Element of REAL
[f,j] is set
{f,j} is non empty set
{f} is non empty set
{{f,j},{f}} is non empty set
c . [f,j] is V24() ext-real real Element of REAL
t . [f,j] is V24() ext-real real Element of REAL
X is non empty set
[:X,REAL:] is non empty Relation-like set
bool [:X,REAL:] is non empty set
Q is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
RP is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
min (Q,RP) is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
min (RP,Q) is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
Q is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
RP is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
max (Q,RP) is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
max (RP,Q) is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
X is non empty set
[:X,REAL:] is non empty Relation-like set
bool [:X,REAL:] is non empty set
R is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
S is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
(X,R,S) is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
Q is Element of X
(X,R,S) . Q is V24() ext-real real Element of REAL
R . Q is V24() ext-real real Element of REAL
(X,R,S) . Q is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R . Q is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
S . Q is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min ((R . Q),(S . Q)) is V24() ext-real real set
X is non empty set
[:X,REAL:] is non empty Relation-like set
bool [:X,REAL:] is non empty set
R is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
S is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
(X,R,S) is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
Q is Element of X
R . Q is V24() ext-real real Element of REAL
(X,R,S) . Q is V24() ext-real real Element of REAL
(X,R,S) . Q is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R . Q is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
S . Q is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
max ((R . Q),(S . Q)) is V24() ext-real real set
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
Imf (X,X) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
S is Element of X
R . (S,S) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,S] is set
{S,S} is non empty set
{S} is non empty set
{{S,S},{S}} is non empty set
R . [S,S] is set
(Imf (X,X)) . (S,S) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(Imf (X,X)) . [S,S] is set
S is Element of X
Q is Element of X
(Imf (X,X)) . (S,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,Q] is set
{S,Q} is non empty set
{S} is non empty set
{{S,Q},{S}} is non empty set
(Imf (X,X)) . [S,Q] is set
R . (S,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R . [S,Q] is set
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
converse R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
S is Element of X
Q is Element of X
R . (S,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,Q] is set
{S,Q} is non empty set
{S} is non empty set
{{S,Q},{S}} is non empty set
R . [S,Q] is set
R . (Q,S) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[Q,S] is set
{Q,S} is non empty set
{Q} is non empty set
{{Q,S},{Q}} is non empty set
R . [Q,S] is set
dom R is non empty Relation-like X -defined X -valued Element of bool [:X,X:]
bool [:X,X:] is non empty set
S is set
Q is set
[S,Q] is set
{S,Q} is non empty set
{S} is non empty set
{{S,Q},{S}} is non empty set
(converse R) . (S,Q) is V24() ext-real real Element of REAL
(converse R) . [S,Q] is set
R . (S,Q) is V24() ext-real real Element of REAL
R . [S,Q] is set
RP is Element of X
c is Element of X
R . (RP,c) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[RP,c] is set
{RP,c} is non empty set
{RP} is non empty set
{{RP,c},{RP}} is non empty set
R . [RP,c] is set
R . (c,RP) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[c,RP] is set
{c,RP} is non empty set
{c} is non empty set
{{c,RP},{c}} is non empty set
R . [c,RP] is set
dom (converse R) is non empty Relation-like X -defined X -valued Element of bool [:X,X:]
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
X is non empty set
R is non empty set
[:X,R:] is non empty Relation-like set
[:[:X,R:],REAL:] is non empty Relation-like set
bool [:[:X,R:],REAL:] is non empty set
S is non empty set
[:R,S:] is non empty Relation-like set
[:[:R,S:],REAL:] is non empty Relation-like set
bool [:[:R,S:],REAL:] is non empty set
Q is non empty Relation-like [:X,R:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,R:],REAL:]
RP is non empty Relation-like [:R,S:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:R,S:],REAL:]
c is Element of X
t is Element of S
min (Q,RP,c,t) is non empty Relation-like R -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:R,REAL:]
[:R,REAL:] is non empty Relation-like set
bool [:R,REAL:] is non empty set
rng (min (Q,RP,c,t)) is non empty V43() V44() V45() Element of bool REAL
{ ((Q . [c,b₁]) "/\" (RP . [b₁,t])) where b₁ is Element of R : verum } is set
dom (min (Q,RP,c,t)) is non empty Element of bool R
bool R is non empty set
[:(dom (min (Q,RP,c,t))),(rng (min (Q,RP,c,t))):] is non empty Relation-like set
bool [:(dom (min (Q,RP,c,t))),(rng (min (Q,RP,c,t))):] is non empty set
n is set
j is Element of R
[c,j] is Element of [:X,R:]
{c,j} is non empty set
{c} is non empty set
{{c,j},{c}} is non empty set
Q . [c,j] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[j,t] is Element of [:R,S:]
{j,t} is non empty set
{j} is non empty set
{{j,t},{j}} is non empty set
RP . [j,t] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(Q . [c,j]) "/\" (RP . [j,t]) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min ((Q . [c,j]),(RP . [j,t])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(min (Q,RP,c,t)) . j is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
j is Element of R
(min (Q,RP,c,t)) . j is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[c,j] is Element of [:X,R:]
{c,j} is non empty set
{{c,j},{c}} is non empty set
Q . [c,j] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[j,t] is Element of [:R,S:]
{j,t} is non empty set
{j} is non empty set
{{j,t},{j}} is non empty set
RP . [j,t] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(Q . [c,j]) "/\" (RP . [j,t]) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min ((Q . [c,j]),(RP . [j,t])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
R (#) R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
S is Element of X
Q is Element of X
[S,Q] is Element of [:X,X:]
{S,Q} is non empty set
{S} is non empty set
{{S,Q},{S}} is non empty set
R . [S,Q] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
RP is Element of X
[Q,RP] is Element of [:X,X:]
{Q,RP} is non empty set
{Q} is non empty set
{{Q,RP},{Q}} is non empty set
R . [Q,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(R . [S,Q]) "/\" (R . [Q,RP]) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min ((R . [S,Q]),(R . [Q,RP])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,RP] is Element of [:X,X:]
{S,RP} is non empty set
{{S,RP},{S}} is non empty set
R . [S,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R . (S,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,Q] is set
R . [S,Q] is set
R . (Q,RP) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[Q,RP] is set
R . [Q,RP] is set
(R . (S,Q)) "/\" (R . (Q,RP)) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min ((R . (S,Q)),(R . (Q,RP))) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
{ ((R . (S,b₁)) "/\" (R . (b₁,RP))) where b₁ is Element of X : verum } is set
"\/" ( { ((R . (S,b₁)) "/\" (R . (b₁,RP))) where b₁ is Element of X : verum } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(R (#) R) . (S,RP) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,RP] is set
(R (#) R) . [S,RP] is set
R . (S,RP) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R . [S,RP] is set
S is Element of X
Q is Element of X
(R (#) R) . (S,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,Q] is set
{S,Q} is non empty set
{S} is non empty set
{{S,Q},{S}} is non empty set
(R (#) R) . [S,Q] is set
R . (S,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R . [S,Q] is set
min (R,R,S,Q) is non empty Relation-like X -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:X,REAL:]
[:X,REAL:] is non empty Relation-like set
bool [:X,REAL:] is non empty set
rng (min (R,R,S,Q)) is non empty V43() V44() V45() Element of bool REAL
[S,Q] is Element of [:X,X:]
R . [S,Q] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
c is V24() ext-real real set
{ ((R . [S,b₁]) "/\" (R . [b₁,Q])) where b₁ is Element of X : verum } is set
t is Element of X
[S,t] is Element of [:X,X:]
{S,t} is non empty set
{{S,t},{S}} is non empty set
R . [S,t] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[t,Q] is Element of [:X,X:]
{t,Q} is non empty set
{t} is non empty set
{{t,Q},{t}} is non empty set
R . [t,Q] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(R . [S,t]) "/\" (R . [t,Q]) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min ((R . [S,t]),(R . [t,Q])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
upper_bound (rng (min (R,R,S,Q))) is V24() ext-real real Element of REAL
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
X is non empty set
Imf (X,X) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
R is Element of X
S is Element of X
(Imf (X,X)) . (R,S) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[R,S] is set
{R,S} is non empty set
{R} is non empty set
{{R,S},{R}} is non empty set
(Imf (X,X)) . [R,S] is set
(Imf (X,X)) . (S,R) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,R] is set
{S,R} is non empty set
{S} is non empty set
{{S,R},{S}} is non empty set
(Imf (X,X)) . [S,R] is set
R is Element of X
S is Element of X
[R,S] is Element of [:X,X:]
{R,S} is non empty set
{R} is non empty set
{{R,S},{R}} is non empty set
(Imf (X,X)) . [R,S] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
Q is Element of X
[S,Q] is Element of [:X,X:]
{S,Q} is non empty set
{S} is non empty set
{{S,Q},{S}} is non empty set
(Imf (X,X)) . [S,Q] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
((Imf (X,X)) . [R,S]) "/\" ((Imf (X,X)) . [S,Q]) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min (((Imf (X,X)) . [R,S]),((Imf (X,X)) . [S,Q])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[R,Q] is Element of [:X,X:]
{R,Q} is non empty set
{{R,Q},{R}} is non empty set
(Imf (X,X)) . [R,Q] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(Imf (X,X)) . (R,S) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[R,S] is set
(Imf (X,X)) . [R,S] is set
(Imf (X,X)) . (S,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,Q] is set
(Imf (X,X)) . [S,Q] is set
min (((Imf (X,X)) . (R,S)),((Imf (X,X)) . (S,Q))) is V24() ext-real real set
((Imf (X,X)) . (R,S)) "/\" ((Imf (X,X)) . (S,Q)) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min (((Imf (X,X)) . (R,S)),((Imf (X,X)) . (S,Q))) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(Imf (X,X)) . (R,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[R,Q] is set
(Imf (X,X)) . [R,Q] is set
(Imf (X,X)) . (R,S) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[R,S] is set
(Imf (X,X)) . [R,S] is set
(Imf (X,X)) . (S,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,Q] is set
(Imf (X,X)) . [S,Q] is set
min (((Imf (X,X)) . (R,S)),((Imf (X,X)) . (S,Q))) is V24() ext-real real set
min (((Imf (X,X)) . (R,S)),0) is V24() ext-real real set
min (0,0) is ordinal natural V24() ext-real non negative real set
((Imf (X,X)) . (R,S)) "/\" ((Imf (X,X)) . (S,Q)) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min (((Imf (X,X)) . (R,S)),((Imf (X,X)) . (S,Q))) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(Imf (X,X)) . (R,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[R,Q] is set
(Imf (X,X)) . [R,Q] is set
(Imf (X,X)) . (R,S) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[R,S] is set
(Imf (X,X)) . [R,S] is set
(Imf (X,X)) . (S,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,Q] is set
(Imf (X,X)) . [S,Q] is set
min (((Imf (X,X)) . (R,S)),((Imf (X,X)) . (S,Q))) is V24() ext-real real set
min (((Imf (X,X)) . (R,S)),0) is V24() ext-real real set
min (1,0) is ordinal natural V24() ext-real non negative real set
((Imf (X,X)) . (R,S)) "/\" ((Imf (X,X)) . (S,Q)) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min (((Imf (X,X)) . (R,S)),((Imf (X,X)) . (S,Q))) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(Imf (X,X)) . (R,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[R,Q] is set
(Imf (X,X)) . [R,Q] is set
(Imf (X,X)) . (R,S) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[R,S] is set
(Imf (X,X)) . [R,S] is set
(Imf (X,X)) . (S,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,Q] is set
(Imf (X,X)) . [S,Q] is set
min (((Imf (X,X)) . (R,S)),((Imf (X,X)) . (S,Q))) is V24() ext-real real set
min (((Imf (X,X)) . (R,S)),1) is V24() ext-real real set
min (0,1) is ordinal natural V24() ext-real non negative real set
((Imf (X,X)) . (R,S)) "/\" ((Imf (X,X)) . (S,Q)) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min (((Imf (X,X)) . (R,S)),((Imf (X,X)) . (S,Q))) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(Imf (X,X)) . (R,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[R,Q] is set
(Imf (X,X)) . [R,Q] is set
(Imf (X,X)) . (R,S) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[R,S] is set
(Imf (X,X)) . [R,S] is set
(Imf (X,X)) . (S,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,Q] is set
(Imf (X,X)) . [S,Q] is set
min (((Imf (X,X)) . (R,S)),((Imf (X,X)) . (S,Q))) is V24() ext-real real set
min (((Imf (X,X)) . (R,S)),0) is V24() ext-real real set
min (0,0) is ordinal natural V24() ext-real non negative real set
((Imf (X,X)) . (R,S)) "/\" ((Imf (X,X)) . (S,Q)) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min (((Imf (X,X)) . (R,S)),((Imf (X,X)) . (S,Q))) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(Imf (X,X)) . (R,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[R,Q] is set
(Imf (X,X)) . [R,Q] is set
R is Element of X
S is Element of X
(Imf (X,X)) . (R,S) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[R,S] is set
{R,S} is non empty set
{R} is non empty set
{{R,S},{R}} is non empty set
(Imf (X,X)) . [R,S] is set
(Imf (X,X)) . (S,R) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,R] is set
{S,R} is non empty set
{S} is non empty set
{{S,R},{S}} is non empty set
(Imf (X,X)) . [S,R] is set
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
Imf (X,X) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued (X) (X) (X) (X) Element of bool [:[:X,X:],REAL:]
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
S is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
([:X,X:],R,S) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
converse ([:X,X:],R,S) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
converse R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
converse S is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
S is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
([:X,X:],R,S) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
converse ([:X,X:],R,S) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
converse R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
converse S is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued (X) Element of bool [:[:X,X:],REAL:]
S is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued (X) Element of bool [:[:X,X:],REAL:]
([:X,X:],R,S) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
converse ([:X,X:],R,S) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
([:X,X:],R,S) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
converse ([:X,X:],R,S) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
S is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
([:X,X:],R,S) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
([:X,X:],R,S) (#) ([:X,X:],R,S) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
Q is Element of X
RP is Element of X
(([:X,X:],R,S) (#) ([:X,X:],R,S)) . (Q,RP) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[Q,RP] is set
{Q,RP} is non empty set
{Q} is non empty set
{{Q,RP},{Q}} is non empty set
(([:X,X:],R,S) (#) ([:X,X:],R,S)) . [Q,RP] is set
([:X,X:],R,S) . (Q,RP) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
([:X,X:],R,S) . [Q,RP] is set
R (#) S is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
S (#) S is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
([:X,X:],(R (#) S),(S (#) S)) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
[Q,RP] is Element of [:X,X:]
([:X,X:],(R (#) S),(S (#) S)) . [Q,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(S (#) S) . [Q,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(R (#) S) . [Q,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min (((S (#) S) . [Q,RP]),((R (#) S) . [Q,RP])) is V24() ext-real real set
(S (#) S) . (Q,RP) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(S (#) S) . [Q,RP] is set
S . (Q,RP) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
S . [Q,RP] is set
S . [Q,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R (#) R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
S (#) R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
([:X,X:],(R (#) R),(S (#) R)) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
([:X,X:],(R (#) R),(S (#) R)) . [Q,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(R (#) R) . [Q,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(S (#) R) . [Q,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min (((R (#) R) . [Q,RP]),((S (#) R) . [Q,RP])) is V24() ext-real real set
(R (#) R) . (Q,RP) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(R (#) R) . [Q,RP] is set
R . (Q,RP) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R . [Q,RP] is set
R . [Q,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min ((([:X,X:],(R (#) R),(S (#) R)) . [Q,RP]),(([:X,X:],(R (#) S),(S (#) S)) . [Q,RP])) is V24() ext-real real set
min ((R . [Q,RP]),(S . [Q,RP])) is V24() ext-real real set
([:X,X:],R,S) (#) R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
([:X,X:],R,S) (#) S is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
([:X,X:],(([:X,X:],R,S) (#) R),(([:X,X:],R,S) (#) S)) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(([:X,X:],R,S) (#) ([:X,X:],R,S)) . [Q,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
([:X,X:],(([:X,X:],R,S) (#) R),(([:X,X:],R,S) (#) S)) . [Q,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(([:X,X:],R,S) (#) S) . [Q,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(([:X,X:],R,S) (#) R) . [Q,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min (((([:X,X:],R,S) (#) R) . [Q,RP]),((([:X,X:],R,S) (#) S) . [Q,RP])) is V24() ext-real real set
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued (X) Element of bool [:[:X,X:],REAL:]
S is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued (X) Element of bool [:[:X,X:],REAL:]
([:X,X:],R,S) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
([:X,X:],R,S) (#) ([:X,X:],R,S) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
X is set
R is non empty set
chi (X,R) is Relation-like [.0,1.] -valued Function-like set
[:R,REAL:] is non empty Relation-like set
bool [:R,REAL:] is non empty set
chi (X,R) is Relation-like R -defined REAL -valued [.0,1.] -valued Function-like Element of bool [:R,REAL:]
dom (chi (X,R)) is Element of bool R
bool R is non empty set
X is non empty set
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
R is Relation-like X -defined X -valued Element of bool [:X,X:]
(R,[:X,X:]) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
S is Element of X
(R,[:X,X:]) . (S,S) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,S] is set
{S,S} is non empty set
{S} is non empty set
{{S,S},{S}} is non empty set
(R,[:X,X:]) . [S,S] is set
[S,S] is Element of [:X,X:]
X is non empty set
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
R is Relation-like X -defined X -valued Element of bool [:X,X:]
(R,[:X,X:]) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
field R is set
S is Element of X
Q is Element of X
(R,[:X,X:]) . (S,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,Q] is set
{S,Q} is non empty set
{S} is non empty set
{{S,Q},{S}} is non empty set
(R,[:X,X:]) . [S,Q] is set
(R,[:X,X:]) . (Q,S) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[Q,S] is set
{Q,S} is non empty set
{Q} is non empty set
{{Q,S},{Q}} is non empty set
(R,[:X,X:]) . [Q,S] is set
[S,Q] is Element of [:X,X:]
[Q,S] is Element of [:X,X:]
X is non empty set
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
R is Relation-like X -defined X -valued Element of bool [:X,X:]
(R,[:X,X:]) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
field R is set
S is Element of X
Q is Element of X
(R,[:X,X:]) . (S,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,Q] is set
{S,Q} is non empty set
{S} is non empty set
{{S,Q},{S}} is non empty set
(R,[:X,X:]) . [S,Q] is set
(R,[:X,X:]) . (Q,S) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[Q,S] is set
{Q,S} is non empty set
{Q} is non empty set
{{Q,S},{Q}} is non empty set
(R,[:X,X:]) . [Q,S] is set
[S,Q] is Element of [:X,X:]
[Q,S] is Element of [:X,X:]
(R,[:X,X:]) . [S,Q] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(R,[:X,X:]) . [S,Q] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
X is non empty set
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
R is Relation-like X -defined X -valued Element of bool [:X,X:]
(R,[:X,X:]) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
S is Element of X
Q is Element of X
[S,Q] is Element of [:X,X:]
{S,Q} is non empty set
{S} is non empty set
{{S,Q},{S}} is non empty set
(R,[:X,X:]) . [S,Q] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
RP is Element of X
[Q,RP] is Element of [:X,X:]
{Q,RP} is non empty set
{Q} is non empty set
{{Q,RP},{Q}} is non empty set
(R,[:X,X:]) . [Q,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
((R,[:X,X:]) . [S,Q]) "/\" ((R,[:X,X:]) . [Q,RP]) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min (((R,[:X,X:]) . [S,Q]),((R,[:X,X:]) . [Q,RP])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,RP] is Element of [:X,X:]
{S,RP} is non empty set
{{S,RP},{S}} is non empty set
(R,[:X,X:]) . [S,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
field R is set
min (1,((R,[:X,X:]) . [Q,RP])) is V24() ext-real real set
min (1,1) is ordinal natural V24() ext-real non negative real set
min (1,((R,[:X,X:]) . [Q,RP])) is V24() ext-real real set
min (1,0) is ordinal natural V24() ext-real non negative real set
min (0,((R,[:X,X:]) . [Q,RP])) is V24() ext-real real set
min (0,1) is ordinal natural V24() ext-real non negative real set
min (0,((R,[:X,X:]) . [Q,RP])) is V24() ext-real real set
min (0,0) is ordinal natural V24() ext-real non negative real set
X is non empty set
Zmf (X,X) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
R is Element of X
S is Element of X
(Zmf (X,X)) . (R,S) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[R,S] is set
{R,S} is non empty set
{R} is non empty set
{{R,S},{R}} is non empty set
(Zmf (X,X)) . [R,S] is set
(Zmf (X,X)) . (S,R) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,R] is set
{S,R} is non empty set
{S} is non empty set
{{S,R},{S}} is non empty set
(Zmf (X,X)) . [S,R] is set
[R,S] is Element of [:X,X:]
(Zmf (X,X)) . [R,S] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,R] is Element of [:X,X:]
(Zmf (X,X)) . [S,R] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R is Element of X
S is Element of X
(Zmf (X,X)) . (R,S) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[R,S] is set
{R,S} is non empty set
{R} is non empty set
{{R,S},{R}} is non empty set
(Zmf (X,X)) . [R,S] is set
(Zmf (X,X)) . (S,R) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,R] is set
{S,R} is non empty set
{S} is non empty set
{{S,R},{S}} is non empty set
(Zmf (X,X)) . [S,R] is set
[R,S] is Element of [:X,X:]
(Zmf (X,X)) . [R,S] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R is Element of X
S is Element of X
[R,S] is Element of [:X,X:]
{R,S} is non empty set
{R} is non empty set
{{R,S},{R}} is non empty set
(Zmf (X,X)) . [R,S] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
Q is Element of X
[S,Q] is Element of [:X,X:]
{S,Q} is non empty set
{S} is non empty set
{{S,Q},{S}} is non empty set
(Zmf (X,X)) . [S,Q] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
((Zmf (X,X)) . [R,S]) "/\" ((Zmf (X,X)) . [S,Q]) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min (((Zmf (X,X)) . [R,S]),((Zmf (X,X)) . [S,Q])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[R,Q] is Element of [:X,X:]
{R,Q} is non empty set
{{R,Q},{R}} is non empty set
(Zmf (X,X)) . [R,Q] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min (0,((Zmf (X,X)) . [S,Q])) is V24() ext-real real set
min (0,0) is ordinal natural V24() ext-real non negative real set
X is non empty set
Umf (X,X) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
R is Element of X
S is Element of X
(Umf (X,X)) . (R,S) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[R,S] is set
{R,S} is non empty set
{R} is non empty set
{{R,S},{R}} is non empty set
(Umf (X,X)) . [R,S] is set
(Umf (X,X)) . (S,R) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,R] is set
{S,R} is non empty set
{S} is non empty set
{{S,R},{S}} is non empty set
(Umf (X,X)) . [S,R] is set
[R,S] is Element of [:X,X:]
(Umf (X,X)) . [R,S] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[S,R] is Element of [:X,X:]
(Umf (X,X)) . [S,R] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R is Element of X
S is Element of X
[R,S] is Element of [:X,X:]
{R,S} is non empty set
{R} is non empty set
{{R,S},{R}} is non empty set
(Umf (X,X)) . [R,S] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
Q is Element of X
[S,Q] is Element of [:X,X:]
{S,Q} is non empty set
{S} is non empty set
{{S,Q},{S}} is non empty set
(Umf (X,X)) . [S,Q] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
((Umf (X,X)) . [R,S]) "/\" ((Umf (X,X)) . [S,Q]) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min (((Umf (X,X)) . [R,S]),((Umf (X,X)) . [S,Q])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[R,Q] is Element of [:X,X:]
{R,Q} is non empty set
{{R,Q},{R}} is non empty set
(Umf (X,X)) . [R,Q] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min (1,((Umf (X,X)) . [S,Q])) is V24() ext-real real set
min (1,1) is ordinal natural V24() ext-real non negative real set
R is Element of X
(Umf (X,X)) . (R,R) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[R,R] is set
{R,R} is non empty set
{R} is non empty set
{{R,R},{R}} is non empty set
(Umf (X,X)) . [R,R] is set
[R,R] is Element of [:X,X:]
(Umf (X,X)) . [R,R] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
converse R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
([:X,X:],R,(converse R)) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
Q is Element of X
RP is Element of X
([:X,X:],R,(converse R)) . (Q,RP) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[Q,RP] is set
{Q,RP} is non empty set
{Q} is non empty set
{{Q,RP},{Q}} is non empty set
([:X,X:],R,(converse R)) . [Q,RP] is set
([:X,X:],R,(converse R)) . (RP,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[RP,Q] is set
{RP,Q} is non empty set
{RP} is non empty set
{{RP,Q},{RP}} is non empty set
([:X,X:],R,(converse R)) . [RP,Q] is set
[Q,RP] is Element of [:X,X:]
([:X,X:],R,(converse R)) . [Q,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R . (Q,RP) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R . [Q,RP] is set
(converse R) . (Q,RP) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(converse R) . [Q,RP] is set
max ((R . (Q,RP)),((converse R) . (Q,RP))) is V24() ext-real real set
R . (RP,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R . [RP,Q] is set
max ((R . (Q,RP)),(R . (RP,Q))) is V24() ext-real real set
(converse R) . (RP,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(converse R) . [RP,Q] is set
max (((converse R) . (RP,Q)),(R . (RP,Q))) is V24() ext-real real set
[RP,Q] is Element of [:X,X:]
([:X,X:],R,(converse R)) . [RP,Q] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
converse R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
([:X,X:],R,(converse R)) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
Q is Element of X
RP is Element of X
([:X,X:],R,(converse R)) . (Q,RP) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[Q,RP] is set
{Q,RP} is non empty set
{Q} is non empty set
{{Q,RP},{Q}} is non empty set
([:X,X:],R,(converse R)) . [Q,RP] is set
([:X,X:],R,(converse R)) . (RP,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[RP,Q] is set
{RP,Q} is non empty set
{RP} is non empty set
{{RP,Q},{RP}} is non empty set
([:X,X:],R,(converse R)) . [RP,Q] is set
[Q,RP] is Element of [:X,X:]
([:X,X:],R,(converse R)) . [Q,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R . (Q,RP) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R . [Q,RP] is set
(converse R) . (Q,RP) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(converse R) . [Q,RP] is set
min ((R . (Q,RP)),((converse R) . (Q,RP))) is V24() ext-real real set
R . (RP,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R . [RP,Q] is set
min ((R . (Q,RP)),(R . (RP,Q))) is V24() ext-real real set
(converse R) . (RP,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(converse R) . [RP,Q] is set
min (((converse R) . (RP,Q)),(R . (RP,Q))) is V24() ext-real real set
[RP,Q] is Element of [:X,X:]
([:X,X:],R,(converse R)) . [RP,Q] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
converse R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
([:X,X:],R,(converse R)) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
S is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
Q is Element of X
RP is Element of X
([:X,X:],R,(converse R)) . (Q,RP) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[Q,RP] is set
{Q,RP} is non empty set
{Q} is non empty set
{{Q,RP},{Q}} is non empty set
([:X,X:],R,(converse R)) . [Q,RP] is set
S . (Q,RP) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
S . [Q,RP] is set
[RP,Q] is Element of [:X,X:]
{RP,Q} is non empty set
{RP} is non empty set
{{RP,Q},{RP}} is non empty set
R . [RP,Q] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
S . [RP,Q] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R . (RP,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[RP,Q] is set
R . [RP,Q] is set
S . (RP,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
S . [RP,Q] is set
[Q,RP] is Element of [:X,X:]
R . [Q,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
S . [Q,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R . (Q,RP) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R . [Q,RP] is set
max ((R . (Q,RP)),(R . (RP,Q))) is V24() ext-real real set
(converse R) . (Q,RP) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(converse R) . [Q,RP] is set
max ((R . (Q,RP)),((converse R) . (Q,RP))) is V24() ext-real real set
(converse R) . [Q,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
max ((R . [Q,RP]),((converse R) . [Q,RP])) is V24() ext-real real set
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
converse R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
([:X,X:],R,(converse R)) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
S is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
Q is Element of X
RP is Element of X
S . (Q,RP) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[Q,RP] is set
{Q,RP} is non empty set
{Q} is non empty set
{{Q,RP},{Q}} is non empty set
S . [Q,RP] is set
([:X,X:],R,(converse R)) . (Q,RP) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
([:X,X:],R,(converse R)) . [Q,RP] is set
[RP,Q] is Element of [:X,X:]
{RP,Q} is non empty set
{RP} is non empty set
{{RP,Q},{RP}} is non empty set
S . [RP,Q] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R . [RP,Q] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
S . (RP,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[RP,Q] is set
S . [RP,Q] is set
R . (RP,Q) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R . [RP,Q] is set
[Q,RP] is Element of [:X,X:]
S . [Q,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R . [Q,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R . (Q,RP) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R . [Q,RP] is set
min ((R . (Q,RP)),(R . (RP,Q))) is V24() ext-real real set
(converse R) . (Q,RP) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(converse R) . [Q,RP] is set
min ((R . (Q,RP)),((converse R) . (Q,RP))) is V24() ext-real real set
(converse R) . [Q,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min ((R . [Q,RP]),((converse R) . [Q,RP])) is V24() ext-real real set
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
Funcs ([:X,X:],[.0,1.]) is non empty functional FUNCTION_DOMAIN of [:X,X:],[.0,1.]
[:NAT,(Funcs ([:X,X:],[.0,1.])):] is Relation-like set
bool [:NAT,(Funcs ([:X,X:],[.0,1.])):] is non empty set
S is ordinal natural V24() ext-real non negative real set
Imf (X,X) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued (X) (X) (X) (X) Element of bool [:[:X,X:],REAL:]
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
FuzzyLattice [:X,X:] is non empty V138() reflexive transitive antisymmetric with_suprema with_infima complete Heyting L14()
the carrier of (FuzzyLattice [:X,X:]) is non empty set
c is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT
t is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
@ t is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(@ t) (#) R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
([:X,X:],((@ t) (#) R)) @ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
n is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
[:NAT, the carrier of (FuzzyLattice [:X,X:]):] is Relation-like set
bool [:NAT, the carrier of (FuzzyLattice [:X,X:]):] is non empty set
([:X,X:],(Imf (X,X))) @ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
c is Relation-like NAT -defined the carrier of (FuzzyLattice [:X,X:]) -valued Function-like total quasi_total Element of bool [:NAT, the carrier of (FuzzyLattice [:X,X:]):]
c . 0 is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
t is Relation-like NAT -defined Funcs ([:X,X:],[.0,1.]) -valued Function-like total quasi_total Element of bool [:NAT,(Funcs ([:X,X:],[.0,1.])):]
Q is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT
t . Q is Element of Funcs ([:X,X:],[.0,1.])
i is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
@ i is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
n is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
t . S is Element of Funcs ([:X,X:],[.0,1.])
t . 0 is Element of Funcs ([:X,X:],[.0,1.])
j is ordinal natural V24() ext-real non negative real set
t . j is Element of Funcs ([:X,X:],[.0,1.])
j + 1 is non empty ordinal natural V24() ext-real positive non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT
t . (j + 1) is Element of Funcs ([:X,X:],[.0,1.])
f is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT
t . f is Element of Funcs ([:X,X:],[.0,1.])
f is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
@ f is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
b is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
b (#) R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
f + 1 is non empty ordinal natural V24() ext-real positive non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT
t . (f + 1) is Element of Funcs ([:X,X:],[.0,1.])
c₁₄ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
@ c₁₄ is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(@ c₁₄) (#) R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
Q is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
RP is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
c is Relation-like NAT -defined Funcs ([:X,X:],[.0,1.]) -valued Function-like total quasi_total Element of bool [:NAT,(Funcs ([:X,X:],[.0,1.])):]
c . S is Element of Funcs ([:X,X:],[.0,1.])
c . 0 is Element of Funcs ([:X,X:],[.0,1.])
t is Relation-like NAT -defined Funcs ([:X,X:],[.0,1.]) -valued Function-like total quasi_total Element of bool [:NAT,(Funcs ([:X,X:],[.0,1.])):]
t . S is Element of Funcs ([:X,X:],[.0,1.])
t . 0 is Element of Funcs ([:X,X:],[.0,1.])
i is ordinal natural V24() ext-real non negative real set
c . i is Element of Funcs ([:X,X:],[.0,1.])
t . i is Element of Funcs ([:X,X:],[.0,1.])
i + 1 is non empty ordinal natural V24() ext-real positive non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT
c . (i + 1) is Element of Funcs ([:X,X:],[.0,1.])
t . (i + 1) is Element of Funcs ([:X,X:],[.0,1.])
n is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
n (#) R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
j is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
j (#) R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
Imf (X,X) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued (X) (X) (X) (X) Element of bool [:[:X,X:],REAL:]
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(Imf (X,X)) (#) R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
dom ((Imf (X,X)) (#) R) is non empty Relation-like X -defined X -valued Element of bool [:X,X:]
bool [:X,X:] is non empty set
S is set
Q is set
[S,Q] is set
{S,Q} is non empty set
{S} is non empty set
{{S,Q},{S}} is non empty set
((Imf (X,X)) (#) R) . (S,Q) is V24() ext-real real Element of REAL
((Imf (X,X)) (#) R) . [S,Q] is set
R . (S,Q) is V24() ext-real real Element of REAL
R . [S,Q] is set
RP is Element of X
c is Element of X
{ (((Imf (X,X)) . (RP,b₁)) "/\" (R . (b₁,c))) where b₁ is Element of X : verum } is set
[RP,c] is Element of [:X,X:]
{RP,c} is non empty set
{RP} is non empty set
{{RP,c},{RP}} is non empty set
R . [RP,c] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
i is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
n is Element of X
(Imf (X,X)) . (RP,n) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[RP,n] is set
{RP,n} is non empty set
{{RP,n},{RP}} is non empty set
(Imf (X,X)) . [RP,n] is set
R . (n,c) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[n,c] is set
{n,c} is non empty set
{n} is non empty set
{{n,c},{n}} is non empty set
R . [n,c] is set
((Imf (X,X)) . (RP,n)) "/\" (R . (n,c)) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min (((Imf (X,X)) . (RP,n)),(R . (n,c))) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[n,c] is Element of [:X,X:]
R . [n,c] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min ((R . [n,c]),1) is V24() ext-real real set
[n,c] is Element of [:X,X:]
R . [n,c] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min ((R . [n,c]),0) is V24() ext-real real set
R . (RP,c) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[RP,c] is set
R . [RP,c] is set
((Imf (X,X)) (#) R) . (RP,c) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[RP,c] is set
((Imf (X,X)) (#) R) . [RP,c] is set
"\/" ( { (((Imf (X,X)) . (RP,b₁)) "/\" (R . (b₁,c))) where b₁ is Element of X : verum } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R . (RP,c) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R . [RP,c] is set
i is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(Imf (X,X)) . (RP,RP) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[RP,RP] is set
{RP,RP} is non empty set
{{RP,RP},{RP}} is non empty set
(Imf (X,X)) . [RP,RP] is set
((Imf (X,X)) . (RP,RP)) "/\" (R . [RP,c]) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min (((Imf (X,X)) . (RP,RP)),(R . [RP,c])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min (1,(R . (RP,c))) is V24() ext-real real set
dom R is non empty Relation-like X -defined X -valued Element of bool [:X,X:]
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
Imf (X,X) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued (X) (X) (X) (X) Element of bool [:[:X,X:],REAL:]
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
R (#) (Imf (X,X)) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
dom (R (#) (Imf (X,X))) is non empty Relation-like X -defined X -valued Element of bool [:X,X:]
bool [:X,X:] is non empty set
S is set
Q is set
[S,Q] is set
{S,Q} is non empty set
{S} is non empty set
{{S,Q},{S}} is non empty set
(R (#) (Imf (X,X))) . (S,Q) is V24() ext-real real Element of REAL
(R (#) (Imf (X,X))) . [S,Q] is set
R . (S,Q) is V24() ext-real real Element of REAL
R . [S,Q] is set
RP is Element of X
c is Element of X
{ ((R . (RP,b₁)) "/\" ((Imf (X,X)) . (b₁,c))) where b₁ is Element of X : verum } is set
[RP,c] is Element of [:X,X:]
{RP,c} is non empty set
{RP} is non empty set
{{RP,c},{RP}} is non empty set
R . [RP,c] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
i is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
n is Element of X
R . (RP,n) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[RP,n] is set
{RP,n} is non empty set
{{RP,n},{RP}} is non empty set
R . [RP,n] is set
(Imf (X,X)) . (n,c) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[n,c] is set
{n,c} is non empty set
{n} is non empty set
{{n,c},{n}} is non empty set
(Imf (X,X)) . [n,c] is set
(R . (RP,n)) "/\" ((Imf (X,X)) . (n,c)) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min ((R . (RP,n)),((Imf (X,X)) . (n,c))) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[RP,n] is Element of [:X,X:]
R . [RP,n] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min ((R . [RP,n]),1) is V24() ext-real real set
[RP,n] is Element of [:X,X:]
R . [RP,n] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min ((R . [RP,n]),0) is V24() ext-real real set
R . (RP,c) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[RP,c] is set
R . [RP,c] is set
(R (#) (Imf (X,X))) . (RP,c) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[RP,c] is set
(R (#) (Imf (X,X))) . [RP,c] is set
"\/" ( { ((R . (RP,b₁)) "/\" ((Imf (X,X)) . (b₁,c))) where b₁ is Element of X : verum } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R . (RP,c) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R . [RP,c] is set
i is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(Imf (X,X)) . (c,c) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[c,c] is set
{c,c} is non empty set
{c} is non empty set
{{c,c},{c}} is non empty set
(Imf (X,X)) . [c,c] is set
(R . [RP,c]) "/\" ((Imf (X,X)) . (c,c)) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min ((R . [RP,c]),((Imf (X,X)) . (c,c))) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min ((R . [RP,c]),1) is V24() ext-real real set
dom R is non empty Relation-like X -defined X -valued Element of bool [:X,X:]
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
Imf (X,X) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued (X) (X) (X) (X) Element of bool [:[:X,X:],REAL:]
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,R,0) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
Funcs ([:X,X:],[.0,1.]) is non empty functional FUNCTION_DOMAIN of [:X,X:],[.0,1.]
[:NAT,(Funcs ([:X,X:],[.0,1.])):] is Relation-like set
bool [:NAT,(Funcs ([:X,X:],[.0,1.])):] is non empty set
S is Relation-like NAT -defined Funcs ([:X,X:],[.0,1.]) -valued Function-like total quasi_total Element of bool [:NAT,(Funcs ([:X,X:],[.0,1.])):]
S . 0 is Element of Funcs ([:X,X:],[.0,1.])
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,R,1) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
Funcs ([:X,X:],[.0,1.]) is non empty functional FUNCTION_DOMAIN of [:X,X:],[.0,1.]
[:NAT,(Funcs ([:X,X:],[.0,1.])):] is Relation-like set
bool [:NAT,(Funcs ([:X,X:],[.0,1.])):] is non empty set
Imf (X,X) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued (X) (X) (X) (X) Element of bool [:[:X,X:],REAL:]
S is Relation-like NAT -defined Funcs ([:X,X:],[.0,1.]) -valued Function-like total quasi_total Element of bool [:NAT,(Funcs ([:X,X:],[.0,1.])):]
S . 1 is Element of Funcs ([:X,X:],[.0,1.])
S . 0 is Element of Funcs ([:X,X:],[.0,1.])
0 + 1 is non empty ordinal natural V24() ext-real positive non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT
S . (0 + 1) is Element of Funcs ([:X,X:],[.0,1.])
Q is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
Q (#) R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
S is ordinal natural V24() ext-real non negative real set
S + 1 is non empty ordinal natural V24() ext-real positive non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT
(X,R,(S + 1)) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,R,S) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,R,S) (#) R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
Funcs ([:X,X:],[.0,1.]) is non empty functional FUNCTION_DOMAIN of [:X,X:],[.0,1.]
[:NAT,(Funcs ([:X,X:],[.0,1.])):] is Relation-like set
bool [:NAT,(Funcs ([:X,X:],[.0,1.])):] is non empty set
Imf (X,X) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued (X) (X) (X) (X) Element of bool [:[:X,X:],REAL:]
Q is Relation-like NAT -defined Funcs ([:X,X:],[.0,1.]) -valued Function-like total quasi_total Element of bool [:NAT,(Funcs ([:X,X:],[.0,1.])):]
Q . (S + 1) is Element of Funcs ([:X,X:],[.0,1.])
Q . 0 is Element of Funcs ([:X,X:],[.0,1.])
Q . S is Element of Funcs ([:X,X:],[.0,1.])
RP is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
RP (#) R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
S is ordinal natural V24() ext-real non negative real set
Q is ordinal natural V24() ext-real non negative real set
S + Q is ordinal natural V24() ext-real non negative real set
(X,R,(S + Q)) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,R,S) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,R,Q) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,R,S) (#) (X,R,Q) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
RP is ordinal natural V24() ext-real non negative real set
S + RP is ordinal natural V24() ext-real non negative real set
(X,R,(S + RP)) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,R,RP) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,R,S) (#) (X,R,RP) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
RP + 1 is non empty ordinal natural V24() ext-real positive non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT
S + (RP + 1) is non empty ordinal natural V24() ext-real positive non negative real set
(X,R,(S + (RP + 1))) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,R,(RP + 1)) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,R,S) (#) (X,R,(RP + 1)) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,R,RP) (#) R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,R,S) (#) ((X,R,RP) (#) R) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,R,(S + RP)) (#) R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(S + RP) + 1 is non empty ordinal natural V24() ext-real positive non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT
(X,R,((S + RP) + 1)) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
S + (RP + 1) is non empty ordinal natural V24() ext-real positive non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT
(X,R,(S + (RP + 1))) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,R,0) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,R,S) (#) (X,R,0) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
Imf (X,X) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued (X) (X) (X) (X) Element of bool [:[:X,X:],REAL:]
(X,R,S) (#) (Imf (X,X)) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
S + 0 is ordinal natural V24() ext-real non negative real set
(X,R,(S + 0)) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
S is ordinal natural V24() ext-real non negative real set
Q is ordinal natural V24() ext-real non negative real set
S * Q is ordinal natural V24() ext-real non negative real set
(X,R,(S * Q)) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,R,Q) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,(X,R,Q),S) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
RP is ordinal natural V24() ext-real non negative real set
RP * Q is ordinal natural V24() ext-real non negative real set
(X,R,(RP * Q)) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,(X,R,Q),RP) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
RP + 1 is non empty ordinal natural V24() ext-real positive non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT
(RP + 1) * Q is ordinal natural V24() ext-real non negative real set
(X,R,((RP + 1) * Q)) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,(X,R,Q),(RP + 1)) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,(X,R,Q),1) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,(X,R,Q),RP) (#) (X,(X,R,Q),1) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,(X,R,Q),RP) (#) (X,R,Q) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(RP + 1) * Q is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT
(X,R,((RP + 1) * Q)) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
1 * Q is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT
(RP * Q) + (1 * Q) is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT
(X,R,((RP * Q) + (1 * Q))) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
0 * Q is empty Relation-like non-empty empty-yielding ordinal natural V24() ext-real non positive non negative real V43() V44() V45() V46() V47() V48() V49() V50() V51() Element of NAT
(X,R,(0 * Q)) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
Imf (X,X) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued (X) (X) (X) (X) Element of bool [:[:X,X:],REAL:]
(X,(X,R,Q),0) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
0 * Q is empty Relation-like non-empty empty-yielding ordinal natural V24() ext-real non positive non negative real V43() V44() V45() V46() V47() V48() V49() set
(X,R,(0 * Q)) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
FuzzyLattice [:X,X:] is non empty V138() reflexive transitive antisymmetric with_suprema with_infima complete Heyting L14()
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
{ (X,R,b₁) where b₁ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } is set
"\/" ( { (X,R,b₁) where b₁ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } ,(FuzzyLattice [:X,X:])) is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
the carrier of (FuzzyLattice [:X,X:]) is non empty set
@ ("\/" ( { (X,R,b₁) where b₁ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } ,(FuzzyLattice [:X,X:]))) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,R) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
FuzzyLattice [:X,X:] is non empty V138() reflexive transitive antisymmetric with_suprema with_infima complete Heyting L14()
{ (X,R,b₁) where b₁ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } is set
"\/" ( { (X,R,b₁) where b₁ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } ,(FuzzyLattice [:X,X:])) is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
the carrier of (FuzzyLattice [:X,X:]) is non empty set
Q is set
c is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT
(X,R,c) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
RP is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
([:X,X:],RP) @ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
c is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
bool the carrier of (FuzzyLattice [:X,X:]) is non empty set
RP is Element of X
c is Element of X
[RP,c] is Element of [:X,X:]
{RP,c} is non empty set
{RP} is non empty set
{{RP,c},{RP}} is non empty set
(X,R) . [RP,c] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
pi ( { (X,R,b₁) where b₁ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } ,[RP,c]) is set
"\/" ((pi ( { (X,R,b₁) where b₁ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } ,[RP,c])),(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[:X,X:] --> (RealPoset [.0,1.]) is non empty Relation-like [:X,X:] -defined {(RealPoset [.0,1.])} -valued Function-like total quasi_total V197() V201() V202() Element of bool [:[:X,X:],{(RealPoset [.0,1.])}:]
{(RealPoset [.0,1.])} is non empty set
[:[:X,X:],{(RealPoset [.0,1.])}:] is non empty Relation-like set
bool [:[:X,X:],{(RealPoset [.0,1.])}:] is non empty set
i is Element of [:X,X:]
([:X,X:] --> (RealPoset [.0,1.])) . i is L14()
(RealPoset [.0,1.]) |^ [:X,X:] is non empty V183() reflexive transitive antisymmetric with_suprema with_infima complete Heyting L14()
product ([:X,X:] --> (RealPoset [.0,1.])) is V183() L14()
Q is Element of bool the carrier of (FuzzyLattice [:X,X:])
"\/" (Q,(FuzzyLattice [:X,X:])) is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
t is Element of [:X,X:]
("\/" (Q,(FuzzyLattice [:X,X:]))) . t is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
([:X,X:] --> (RealPoset [.0,1.])) . t is L14()
pi (Q,t) is set
"\/" ((pi (Q,t)),(([:X,X:] --> (RealPoset [.0,1.])) . t)) is Element of the carrier of (([:X,X:] --> (RealPoset [.0,1.])) . t)
the carrier of (([:X,X:] --> (RealPoset [.0,1.])) . t) is set
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,R) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
FuzzyLattice [:X,X:] is non empty V138() reflexive transitive antisymmetric with_suprema with_infima complete Heyting L14()
{ (X,R,b₁) where b₁ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } is set
"\/" ( { (X,R,b₁) where b₁ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } ,(FuzzyLattice [:X,X:])) is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
the carrier of (FuzzyLattice [:X,X:]) is non empty set
Q is Element of [:X,X:]
R . Q is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(X,R) . Q is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
RP is set
c is set
[RP,c] is set
{RP,c} is non empty set
{RP} is non empty set
{{RP,c},{RP}} is non empty set
(X,R,1) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
t is Element of X
i is Element of X
[t,i] is Element of [:X,X:]
{t,i} is non empty set
{t} is non empty set
{{t,i},{t}} is non empty set
R . [t,i] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
pi ( { (X,R,b₁) where b₁ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } ,[t,i]) is set
(X,R) . [t,i] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
"\/" ((pi ( { (X,R,b₁) where b₁ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } ,[t,i])),(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,R) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
FuzzyLattice [:X,X:] is non empty V138() reflexive transitive antisymmetric with_suprema with_infima complete Heyting L14()
{ (X,R,b₁) where b₁ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } is set
"\/" ( { (X,R,b₁) where b₁ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } ,(FuzzyLattice [:X,X:])) is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
the carrier of (FuzzyLattice [:X,X:]) is non empty set
S is ordinal natural V24() ext-real non negative real set
(X,R,S) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
c is Element of [:X,X:]
(X,R,S) . c is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(X,R) . c is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
t is set
i is set
[t,i] is set
{t,i} is non empty set
{t} is non empty set
{{t,i},{t}} is non empty set
Q is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT
(X,R,Q) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
n is Element of X
j is Element of X
[n,j] is Element of [:X,X:]
{n,j} is non empty set
{n} is non empty set
{{n,j},{n}} is non empty set
(X,R,Q) . [n,j] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
pi ( { (X,R,b₁) where b₁ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } ,[n,j]) is set
(X,R) . [n,j] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
"\/" ((pi ( { (X,R,b₁) where b₁ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } ,[n,j])),(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
X is non empty set
FuzzyLattice X is non empty V138() reflexive transitive antisymmetric with_suprema with_infima complete Heyting L14()
the carrier of (FuzzyLattice X) is non empty set
bool the carrier of (FuzzyLattice X) is non empty set
R is Element of bool the carrier of (FuzzyLattice X)
"\/" (R,(FuzzyLattice X)) is Relation-like Function-like Element of the carrier of (FuzzyLattice X)
S is Element of X
("\/" (R,(FuzzyLattice X))) . S is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
pi (R,S) is set
"\/" ((pi (R,S)),(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
X --> (RealPoset [.0,1.]) is non empty Relation-like X -defined {(RealPoset [.0,1.])} -valued Function-like total quasi_total V197() V201() V202() Element of bool [:X,{(RealPoset [.0,1.])}:]
{(RealPoset [.0,1.])} is non empty set
[:X,{(RealPoset [.0,1.])}:] is non empty Relation-like set
bool [:X,{(RealPoset [.0,1.])}:] is non empty set
Q is Element of X
(X --> (RealPoset [.0,1.])) . Q is L14()
(RealPoset [.0,1.]) |^ X is non empty V183() reflexive transitive antisymmetric with_suprema with_infima complete Heyting L14()
product (X --> (RealPoset [.0,1.])) is V183() L14()
(X --> (RealPoset [.0,1.])) . S is L14()
"\/" ((pi (R,S)),((X --> (RealPoset [.0,1.])) . S)) is Element of the carrier of ((X --> (RealPoset [.0,1.])) . S)
the carrier of ((X --> (RealPoset [.0,1.])) . S) is set
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
FuzzyLattice [:X,X:] is non empty V138() reflexive transitive antisymmetric with_suprema with_infima complete Heyting L14()
the carrier of (FuzzyLattice [:X,X:]) is non empty set
bool the carrier of (FuzzyLattice [:X,X:]) is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
S is Element of bool the carrier of (FuzzyLattice [:X,X:])
"\/" (S,(FuzzyLattice [:X,X:])) is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
@ ("\/" (S,(FuzzyLattice [:X,X:]))) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
Q is Element of X
RP is Element of X
{ ((R . (Q,b₁)) "/\" ((@ ("\/" (S,(FuzzyLattice [:X,X:])))) . (b₁,RP))) where b₁ is Element of X : verum } is set
{ ((R . [Q,b₁]) "/\" ("\/" ((pi (S,[b₁,RP])),(RealPoset [.0,1.])))) where b₁ is Element of X : verum } is set
c is Element of X
[Q,c] is Element of [:X,X:]
{Q,c} is non empty set
{Q} is non empty set
{{Q,c},{Q}} is non empty set
R . [Q,c] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[c,RP] is Element of [:X,X:]
{c,RP} is non empty set
{c} is non empty set
{{c,RP},{c}} is non empty set
(@ ("\/" (S,(FuzzyLattice [:X,X:])))) . [c,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(R . [Q,c]) "/\" ((@ ("\/" (S,(FuzzyLattice [:X,X:])))) . [c,RP]) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min ((R . [Q,c]),((@ ("\/" (S,(FuzzyLattice [:X,X:])))) . [c,RP])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
pi (S,[c,RP]) is set
"\/" ((pi (S,[c,RP])),(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(R . [Q,c]) "/\" ("\/" ((pi (S,[c,RP])),(RealPoset [.0,1.]))) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min ((R . [Q,c]),("\/" ((pi (S,[c,RP])),(RealPoset [.0,1.])))) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
("\/" (S,(FuzzyLattice [:X,X:]))) . [c,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
c is Element of X
R . (Q,c) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[Q,c] is set
{Q,c} is non empty set
{Q} is non empty set
{{Q,c},{Q}} is non empty set
R . [Q,c] is set
(@ ("\/" (S,(FuzzyLattice [:X,X:])))) . (c,RP) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[c,RP] is set
{c,RP} is non empty set
{c} is non empty set
{{c,RP},{c}} is non empty set
(@ ("\/" (S,(FuzzyLattice [:X,X:])))) . [c,RP] is set
(R . (Q,c)) "/\" ((@ ("\/" (S,(FuzzyLattice [:X,X:])))) . (c,RP)) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min ((R . (Q,c)),((@ ("\/" (S,(FuzzyLattice [:X,X:])))) . (c,RP))) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[Q,c] is Element of [:X,X:]
R . [Q,c] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[c,RP] is Element of [:X,X:]
pi (S,[c,RP]) is set
"\/" ((pi (S,[c,RP])),(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(R . [Q,c]) "/\" ("\/" ((pi (S,[c,RP])),(RealPoset [.0,1.]))) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min ((R . [Q,c]),("\/" ((pi (S,[c,RP])),(RealPoset [.0,1.])))) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
{ H₁(b₁) where b₁ is Element of X : S₁[b₁] } is set
{ H₂(b₁) where b₁ is Element of X : S₁[b₁] } is set
X is non empty reflexive transitive antisymmetric with_suprema with_infima complete Heyting L14()
the carrier of X is non empty set
bool the carrier of X is non empty set
R is Element of bool the carrier of X
"\/" (R,X) is Element of the carrier of X
S is Element of the carrier of X
S "/\" ("\/" (R,X)) is Element of the carrier of X
{ (S "/\" b₁) where b₁ is Element of the carrier of X : b₁ in R } is set
"\/" ( { (S "/\" b₁) where b₁ is Element of the carrier of X : b₁ in R } ,X) is Element of the carrier of X
Q is Element of the carrier of X
Q "/\" is non empty Relation-like the carrier of X -defined the carrier of X -valued Function-like total quasi_total Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty Relation-like set
bool [: the carrier of X, the carrier of X:] is non empty set
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
FuzzyLattice [:X,X:] is non empty V138() reflexive transitive antisymmetric with_suprema with_infima complete Heyting L14()
the carrier of (FuzzyLattice [:X,X:]) is non empty set
bool the carrier of (FuzzyLattice [:X,X:]) is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
S is Element of bool the carrier of (FuzzyLattice [:X,X:])
Q is Element of X
RP is Element of X
{ ((R . [Q,b₁]) "/\" ("\/" ((pi (S,[b₁,RP])),(RealPoset [.0,1.])))) where b₁ is Element of X : verum } is set
{ ("\/" ( { ((R . [Q,b₁]) "/\" b₂) where b₂ is V24() ext-real real Element of the carrier of (RealPoset [.0,1.]) : b₂ in pi (S,[b₁,RP]) } ,(RealPoset [.0,1.]))) where b₁ is Element of X : verum } is set
{ ((R . [Q,a₁]) "/\" b₁) where b₁ is V24() ext-real real Element of the carrier of (RealPoset [.0,1.]) : b₁ in pi (S,[a₁,RP]) } is set
"\/" ( { ((R . [Q,a₁]) "/\" b₁) where b₁ is V24() ext-real real Element of the carrier of (RealPoset [.0,1.]) : b₁ in pi (S,[a₁,RP]) } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
c is Element of X
[Q,c] is Element of [:X,X:]
{Q,c} is non empty set
{Q} is non empty set
{{Q,c},{Q}} is non empty set
R . [Q,c] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[c,RP] is Element of [:X,X:]
{c,RP} is non empty set
{c} is non empty set
{{c,RP},{c}} is non empty set
pi (S,[c,RP]) is set
"\/" ((pi (S,[c,RP])),(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(R . [Q,c]) "/\" ("\/" ((pi (S,[c,RP])),(RealPoset [.0,1.]))) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min ((R . [Q,c]),("\/" ((pi (S,[c,RP])),(RealPoset [.0,1.])))) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
{ ((R . [Q,c]) "/\" b₁) where b₁ is V24() ext-real real Element of the carrier of (RealPoset [.0,1.]) : b₁ in pi (S,[c,RP]) } is set
"\/" ( { ((R . [Q,c]) "/\" b₁) where b₁ is V24() ext-real real Element of the carrier of (RealPoset [.0,1.]) : b₁ in pi (S,[c,RP]) } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(RealPoset [.0,1.]) |^ [:X,X:] is non empty V183() reflexive transitive antisymmetric with_suprema with_infima complete Heyting L14()
[:X,X:] --> (RealPoset [.0,1.]) is non empty Relation-like [:X,X:] -defined {(RealPoset [.0,1.])} -valued Function-like total quasi_total V197() V201() V202() Element of bool [:[:X,X:],{(RealPoset [.0,1.])}:]
{(RealPoset [.0,1.])} is non empty set
[:[:X,X:],{(RealPoset [.0,1.])}:] is non empty Relation-like set
bool [:[:X,X:],{(RealPoset [.0,1.])}:] is non empty set
product ([:X,X:] --> (RealPoset [.0,1.])) is V183() L14()
the carrier of (product ([:X,X:] --> (RealPoset [.0,1.]))) is set
bool the carrier of (product ([:X,X:] --> (RealPoset [.0,1.]))) is non empty set
t is Element of bool the carrier of (product ([:X,X:] --> (RealPoset [.0,1.])))
pi (t,[c,RP]) is Element of bool the carrier of (([:X,X:] --> (RealPoset [.0,1.])) . [c,RP])
([:X,X:] --> (RealPoset [.0,1.])) . [c,RP] is L14()
the carrier of (([:X,X:] --> (RealPoset [.0,1.])) . [c,RP]) is set
bool the carrier of (([:X,X:] --> (RealPoset [.0,1.])) . [c,RP]) is non empty set
bool the carrier of (RealPoset [.0,1.]) is non empty set
c is Element of X
[Q,c] is Element of [:X,X:]
{Q,c} is non empty set
{Q} is non empty set
{{Q,c},{Q}} is non empty set
R . [Q,c] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[c,RP] is Element of [:X,X:]
{c,RP} is non empty set
{c} is non empty set
{{c,RP},{c}} is non empty set
pi (S,[c,RP]) is set
"\/" ((pi (S,[c,RP])),(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(R . [Q,c]) "/\" ("\/" ((pi (S,[c,RP])),(RealPoset [.0,1.]))) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min ((R . [Q,c]),("\/" ((pi (S,[c,RP])),(RealPoset [.0,1.])))) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
{ ((R . [Q,c]) "/\" b₁) where b₁ is V24() ext-real real Element of the carrier of (RealPoset [.0,1.]) : b₁ in pi (S,[c,RP]) } is set
"\/" ( { ((R . [Q,c]) "/\" b₁) where b₁ is V24() ext-real real Element of the carrier of (RealPoset [.0,1.]) : b₁ in pi (S,[c,RP]) } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
{ H₁(b₁) where b₁ is Element of X : S₁[b₁] } is set
{ H₂(b₁) where b₁ is Element of X : S₁[b₁] } is set
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
FuzzyLattice [:X,X:] is non empty V138() reflexive transitive antisymmetric with_suprema with_infima complete Heyting L14()
the carrier of (FuzzyLattice [:X,X:]) is non empty set
bool the carrier of (FuzzyLattice [:X,X:]) is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
S is Element of bool the carrier of (FuzzyLattice [:X,X:])
Q is Element of X
RP is Element of X
{ ("\/" ( { ((R . [Q,b₁]) "/\" b₂) where b₂ is V24() ext-real real Element of the carrier of (RealPoset [.0,1.]) : b₂ in pi (S,[b₁,RP]) } ,(RealPoset [.0,1.]))) where b₁ is Element of X : verum } is set
{ ("\/" ( { ((R . [Q,b₁]) "/\" (b₂ . [b₁,RP])) where b₂ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₂ in S } ,(RealPoset [.0,1.]))) where b₁ is Element of X : verum } is set
{ ((R . [Q,a₁]) "/\" b₁) where b₁ is V24() ext-real real Element of the carrier of (RealPoset [.0,1.]) : b₁ in pi (S,[a₁,RP]) } is set
"\/" ( { ((R . [Q,a₁]) "/\" b₁) where b₁ is V24() ext-real real Element of the carrier of (RealPoset [.0,1.]) : b₁ in pi (S,[a₁,RP]) } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
{ ((R . [Q,a₁]) "/\" (b₁ . [a₁,RP])) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } is set
"\/" ( { ((R . [Q,a₁]) "/\" (b₁ . [a₁,RP])) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
i is Element of X
[Q,i] is Element of [:X,X:]
{Q,i} is non empty set
{Q} is non empty set
{{Q,i},{Q}} is non empty set
R . [Q,i] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[i,RP] is Element of [:X,X:]
{i,RP} is non empty set
{i} is non empty set
{{i,RP},{i}} is non empty set
pi (S,[i,RP]) is set
{ ((R . [Q,i]) "/\" b₁) where b₁ is V24() ext-real real Element of the carrier of (RealPoset [.0,1.]) : b₁ in pi (S,[i,RP]) } is set
"\/" ( { ((R . [Q,i]) "/\" b₁) where b₁ is V24() ext-real real Element of the carrier of (RealPoset [.0,1.]) : b₁ in pi (S,[i,RP]) } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
{ ((R . [Q,i]) "/\" (b₁ . [i,RP])) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } is set
"\/" ( { ((R . [Q,i]) "/\" (b₁ . [i,RP])) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
f is set
f is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
f . [i,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(R . [Q,i]) "/\" (f . [i,RP]) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min ((R . [Q,i]),(f . [i,RP])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
f is set
f is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(R . [Q,i]) "/\" f is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min ((R . [Q,i]),f) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
b is Relation-like Function-like set
b . [i,RP] is set
i is Element of X
[Q,i] is Element of [:X,X:]
{Q,i} is non empty set
{Q} is non empty set
{{Q,i},{Q}} is non empty set
R . [Q,i] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[i,RP] is Element of [:X,X:]
{i,RP} is non empty set
{i} is non empty set
{{i,RP},{i}} is non empty set
pi (S,[i,RP]) is set
{ ((R . [Q,i]) "/\" b₁) where b₁ is V24() ext-real real Element of the carrier of (RealPoset [.0,1.]) : b₁ in pi (S,[i,RP]) } is set
"\/" ( { ((R . [Q,i]) "/\" b₁) where b₁ is V24() ext-real real Element of the carrier of (RealPoset [.0,1.]) : b₁ in pi (S,[i,RP]) } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
{ ((R . [Q,i]) "/\" (b₁ . [i,RP])) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } is set
"\/" ( { ((R . [Q,i]) "/\" (b₁ . [i,RP])) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
{ H₁(b₁) where b₁ is Element of X : S₁[b₁] } is set
{ H₂(b₁) where b₁ is Element of X : S₁[b₁] } is set
X is non empty set
R is non empty set
[:X,R:] is non empty Relation-like set
[:[:X,R:],REAL:] is non empty Relation-like set
bool [:[:X,R:],REAL:] is non empty set
S is non empty set
[:R,S:] is non empty Relation-like set
[:[:R,S:],REAL:] is non empty Relation-like set
bool [:[:R,S:],REAL:] is non empty set
Q is non empty Relation-like [:X,R:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,R:],REAL:]
RP is non empty Relation-like [:R,S:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:R,S:],REAL:]
c is Element of X
t is Element of S
min (Q,RP,c,t) is non empty Relation-like R -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:R,REAL:]
[:R,REAL:] is non empty Relation-like set
bool [:R,REAL:] is non empty set
rng (min (Q,RP,c,t)) is non empty V43() V44() V45() Element of bool REAL
{ ((Q . [c,b₁]) "/\" (RP . [b₁,t])) where b₁ is Element of R : verum } is set
dom (min (Q,RP,c,t)) is non empty Element of bool R
bool R is non empty set
[:(dom (min (Q,RP,c,t))),(rng (min (Q,RP,c,t))):] is non empty Relation-like set
bool [:(dom (min (Q,RP,c,t))),(rng (min (Q,RP,c,t))):] is non empty set
n is set
j is Element of R
[c,j] is Element of [:X,R:]
{c,j} is non empty set
{c} is non empty set
{{c,j},{c}} is non empty set
Q . [c,j] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[j,t] is Element of [:R,S:]
{j,t} is non empty set
{j} is non empty set
{{j,t},{j}} is non empty set
RP . [j,t] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(Q . [c,j]) "/\" (RP . [j,t]) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min ((Q . [c,j]),(RP . [j,t])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(min (Q,RP,c,t)) . j is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
j is Element of R
(min (Q,RP,c,t)) . j is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[c,j] is Element of [:X,R:]
{c,j} is non empty set
{{c,j},{c}} is non empty set
Q . [c,j] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[j,t] is Element of [:R,S:]
{j,t} is non empty set
{j} is non empty set
{{j,t},{j}} is non empty set
RP . [j,t] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(Q . [c,j]) "/\" (RP . [j,t]) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min ((Q . [c,j]),(RP . [j,t])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
X is non empty set
R is non empty set
[:X,R:] is non empty Relation-like set
[:[:X,R:],REAL:] is non empty Relation-like set
bool [:[:X,R:],REAL:] is non empty set
S is non empty set
[:R,S:] is non empty Relation-like set
[:[:R,S:],REAL:] is non empty Relation-like set
bool [:[:R,S:],REAL:] is non empty set
[:X,S:] is non empty Relation-like set
Q is non empty Relation-like [:X,R:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,R:],REAL:]
RP is non empty Relation-like [:R,S:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:R,S:],REAL:]
Q (#) RP is non empty Relation-like [:X,S:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,S:],REAL:]
[:[:X,S:],REAL:] is non empty Relation-like set
bool [:[:X,S:],REAL:] is non empty set
c is Element of X
t is Element of S
[c,t] is Element of [:X,S:]
{c,t} is non empty set
{c} is non empty set
{{c,t},{c}} is non empty set
(Q (#) RP) . [c,t] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
{ ((Q . [c,b₁]) "/\" (RP . [b₁,t])) where b₁ is Element of R : verum } is set
"\/" ( { ((Q . [c,b₁]) "/\" (RP . [b₁,t])) where b₁ is Element of R : verum } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(Q (#) RP) . (c,t) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[c,t] is set
(Q (#) RP) . [c,t] is set
min (Q,RP,c,t) is non empty Relation-like R -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:R,REAL:]
[:R,REAL:] is non empty Relation-like set
bool [:R,REAL:] is non empty set
rng (min (Q,RP,c,t)) is non empty V43() V44() V45() Element of bool REAL
upper_bound (rng (min (Q,RP,c,t))) is V24() ext-real real Element of REAL
n is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
j is V24() ext-real real set
f is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
n is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
j is Element of R
[c,j] is Element of [:X,R:]
{c,j} is non empty set
{{c,j},{c}} is non empty set
Q . [c,j] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[j,t] is Element of [:R,S:]
{j,t} is non empty set
{j} is non empty set
{{j,t},{j}} is non empty set
RP . [j,t] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(Q . [c,j]) "/\" (RP . [j,t]) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min ((Q . [c,j]),(RP . [j,t])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
dom (min (Q,RP,c,t)) is non empty Element of bool R
bool R is non empty set
(min (Q,RP,c,t)) . j is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
FuzzyLattice [:X,X:] is non empty V138() reflexive transitive antisymmetric with_suprema with_infima complete Heyting L14()
the carrier of (FuzzyLattice [:X,X:]) is non empty set
bool the carrier of (FuzzyLattice [:X,X:]) is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
S is Element of bool the carrier of (FuzzyLattice [:X,X:])
Q is Element of X
RP is Element of X
{ ("\/" ( { ((R . [Q,b₂]) "/\" (b₁ . [b₂,RP])) where b₂ is Element of X : verum } ,(RealPoset [.0,1.]))) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } is set
{ ("\/" ( { ((R . [Q,b₂]) "/\" ((@ b₁) . [b₂,RP])) where b₂ is Element of X : verum } ,(RealPoset [.0,1.]))) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } is set
{ ((R . [Q,b₁]) "/\" (a₁ . [b₁,RP])) where b₁ is Element of X : verum } is set
"\/" ( { ((R . [Q,b₁]) "/\" (a₁ . [b₁,RP])) where b₁ is Element of X : verum } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
{ ((R . [Q,b₁]) "/\" ((@ a₁) . [b₁,RP])) where b₁ is Element of X : verum } is set
"\/" ( { ((R . [Q,b₁]) "/\" ((@ a₁) . [b₁,RP])) where b₁ is Element of X : verum } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
t is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
{ ((R . [Q,b₁]) "/\" (t . [b₁,RP])) where b₁ is Element of X : verum } is set
"\/" ( { ((R . [Q,b₁]) "/\" (t . [b₁,RP])) where b₁ is Element of X : verum } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
@ t is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
{ ((R . [Q,b₁]) "/\" ((@ t) . [b₁,RP])) where b₁ is Element of X : verum } is set
"\/" ( { ((R . [Q,b₁]) "/\" ((@ t) . [b₁,RP])) where b₁ is Element of X : verum } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
i is Element of X
[Q,i] is Element of [:X,X:]
{Q,i} is non empty set
{Q} is non empty set
{{Q,i},{Q}} is non empty set
R . [Q,i] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[i,RP] is Element of [:X,X:]
{i,RP} is non empty set
{i} is non empty set
{{i,RP},{i}} is non empty set
t . [i,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(R . [Q,i]) "/\" (t . [i,RP]) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min ((R . [Q,i]),(t . [i,RP])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(@ t) . [i,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(R . [Q,i]) "/\" ((@ t) . [i,RP]) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min ((R . [Q,i]),((@ t) . [i,RP])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
{ H₄(b₁) where b₁ is Element of X : S₂[b₁] } is set
{ H₃(b₁) where b₁ is Element of X : S₂[b₁] } is set
t is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
{ ((R . [Q,b₁]) "/\" (t . [b₁,RP])) where b₁ is Element of X : verum } is set
"\/" ( { ((R . [Q,b₁]) "/\" (t . [b₁,RP])) where b₁ is Element of X : verum } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
@ t is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
{ ((R . [Q,b₁]) "/\" ((@ t) . [b₁,RP])) where b₁ is Element of X : verum } is set
"\/" ( { ((R . [Q,b₁]) "/\" ((@ t) . [b₁,RP])) where b₁ is Element of X : verum } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
{ H₁(b₁) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : S₁[b₁] } is set
{ H₂(b₁) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : S₁[b₁] } is set
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
FuzzyLattice [:X,X:] is non empty V138() reflexive transitive antisymmetric with_suprema with_infima complete Heyting L14()
the carrier of (FuzzyLattice [:X,X:]) is non empty set
bool the carrier of (FuzzyLattice [:X,X:]) is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
S is Element of bool the carrier of (FuzzyLattice [:X,X:])
Q is Element of X
RP is Element of X
{ ("\/" ( { ((R . [Q,b₂]) "/\" ((@ b₁) . [b₂,RP])) where b₂ is Element of X : verum } ,(RealPoset [.0,1.]))) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } is set
[Q,RP] is Element of [:X,X:]
{Q,RP} is non empty set
{Q} is non empty set
{{Q,RP},{Q}} is non empty set
{ ((R (#) (@ b₁)) . [Q,RP]) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } is set
{ ((R . [Q,b₁]) "/\" ((@ a₁) . [b₁,RP])) where b₁ is Element of X : verum } is set
"\/" ( { ((R . [Q,b₁]) "/\" ((@ a₁) . [b₁,RP])) where b₁ is Element of X : verum } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
t is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
@ t is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
{ ((R . [Q,b₁]) "/\" ((@ t) . [b₁,RP])) where b₁ is Element of X : verum } is set
"\/" ( { ((R . [Q,b₁]) "/\" ((@ t) . [b₁,RP])) where b₁ is Element of X : verum } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R (#) (@ t) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(R (#) (@ t)) . [Q,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
{ H₁(b₁) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : S₁[b₁] } is set
{ H₂(b₁) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : S₁[b₁] } is set
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
FuzzyLattice [:X,X:] is non empty V138() reflexive transitive antisymmetric with_suprema with_infima complete Heyting L14()
the carrier of (FuzzyLattice [:X,X:]) is non empty set
bool the carrier of (FuzzyLattice [:X,X:]) is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
S is Element of bool the carrier of (FuzzyLattice [:X,X:])
{ (R (#) (@ b₁)) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } is set
Q is Element of X
RP is Element of X
[Q,RP] is Element of [:X,X:]
{Q,RP} is non empty set
{Q} is non empty set
{{Q,RP},{Q}} is non empty set
{ ((R (#) (@ b₁)) . [Q,RP]) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } is set
pi ( { (R (#) (@ b₁)) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } ,[Q,RP]) is set
n is set
j is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
@ j is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
R (#) (@ j) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(R (#) (@ j)) . [Q,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
n is set
j is Relation-like Function-like set
j . [Q,RP] is set
f is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
@ f is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
R (#) (@ f) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
FuzzyLattice [:X,X:] is non empty V138() reflexive transitive antisymmetric with_suprema with_infima complete Heyting L14()
the carrier of (FuzzyLattice [:X,X:]) is non empty set
bool the carrier of (FuzzyLattice [:X,X:]) is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
S is Element of bool the carrier of (FuzzyLattice [:X,X:])
Q is Element of X
RP is Element of X
{ ("\/" ( { ((R . [Q,b₁]) "/\" (b₂ . [b₁,RP])) where b₂ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₂ in S } ,(RealPoset [.0,1.]))) where b₁ is Element of X : verum } is set
"\/" ( { ("\/" ( { ((R . [Q,b₁]) "/\" (b₂ . [b₁,RP])) where b₂ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₂ in S } ,(RealPoset [.0,1.]))) where b₁ is Element of X : verum } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
{ ("\/" ( { ((R . [Q,b₂]) "/\" (b₁ . [b₂,RP])) where b₂ is Element of X : verum } ,(RealPoset [.0,1.]))) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } is set
"\/" ( { ("\/" ( { ((R . [Q,b₂]) "/\" (b₁ . [b₂,RP])) where b₂ is Element of X : verum } ,(RealPoset [.0,1.]))) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
n is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
i is Element of X
[Q,i] is Element of [:X,X:]
{Q,i} is non empty set
{Q} is non empty set
{{Q,i},{Q}} is non empty set
R . [Q,i] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[i,RP] is Element of [:X,X:]
{i,RP} is non empty set
{i} is non empty set
{{i,RP},{i}} is non empty set
n . [i,RP] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(R . [Q,i]) "/\" (n . [i,RP]) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min ((R . [Q,i]),(n . [i,RP])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
{ ("\/" ( { H₁(b₁,b₂) where b₂ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : S₂[b₂] } ,(RealPoset [.0,1.]))) where b₁ is Element of X : S₁[b₁] } is set
"\/" ( { ("\/" ( { H₁(b₁,b₂) where b₂ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : S₂[b₂] } ,(RealPoset [.0,1.]))) where b₁ is Element of X : S₁[b₁] } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
{ ("\/" ( { H₂(b₂,b₁) where b₂ is Element of X : S₁[b₂] } ,(RealPoset [.0,1.]))) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : S₂[b₁] } is set
"\/" ( { ("\/" ( { H₂(b₂,b₁) where b₂ is Element of X : S₁[b₂] } ,(RealPoset [.0,1.]))) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : S₂[b₁] } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
FuzzyLattice [:X,X:] is non empty V138() reflexive transitive antisymmetric with_suprema with_infima complete Heyting L14()
the carrier of (FuzzyLattice [:X,X:]) is non empty set
bool the carrier of (FuzzyLattice [:X,X:]) is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
S is Element of bool the carrier of (FuzzyLattice [:X,X:])
"\/" (S,(FuzzyLattice [:X,X:])) is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
@ ("\/" (S,(FuzzyLattice [:X,X:]))) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
R (#) (@ ("\/" (S,(FuzzyLattice [:X,X:])))) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
{ (R (#) (@ b₁)) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } is set
"\/" ( { (R (#) (@ b₁)) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } ,(FuzzyLattice [:X,X:])) is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
@ ("\/" ( { (R (#) (@ b₁)) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } ,(FuzzyLattice [:X,X:]))) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
c is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
t is Element of X
i is Element of X
(R (#) (@ ("\/" (S,(FuzzyLattice [:X,X:]))))) . (t,i) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[t,i] is set
{t,i} is non empty set
{t} is non empty set
{{t,i},{t}} is non empty set
(R (#) (@ ("\/" (S,(FuzzyLattice [:X,X:]))))) . [t,i] is set
c . (t,i) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
c . [t,i] is set
n is set
j is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
@ j is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
R (#) (@ j) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
([:X,X:],(R (#) (@ j))) @ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
{ ((R . (t,b₁)) "/\" ((@ ("\/" (S,(FuzzyLattice [:X,X:])))) . (b₁,i))) where b₁ is Element of X : verum } is set
"\/" ( { ((R . (t,b₁)) "/\" ((@ ("\/" (S,(FuzzyLattice [:X,X:])))) . (b₁,i))) where b₁ is Element of X : verum } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
{ ((R . [t,b₁]) "/\" ("\/" ((pi (S,[b₁,i])),(RealPoset [.0,1.])))) where b₁ is Element of X : verum } is set
"\/" ( { ((R . [t,b₁]) "/\" ("\/" ((pi (S,[b₁,i])),(RealPoset [.0,1.])))) where b₁ is Element of X : verum } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
{ ("\/" ( { ((R . [t,b₁]) "/\" b₂) where b₂ is V24() ext-real real Element of the carrier of (RealPoset [.0,1.]) : b₂ in pi (S,[b₁,i]) } ,(RealPoset [.0,1.]))) where b₁ is Element of X : verum } is set
"\/" ( { ("\/" ( { ((R . [t,b₁]) "/\" b₂) where b₂ is V24() ext-real real Element of the carrier of (RealPoset [.0,1.]) : b₂ in pi (S,[b₁,i]) } ,(RealPoset [.0,1.]))) where b₁ is Element of X : verum } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
{ ("\/" ( { ((R . [t,b₁]) "/\" (b₂ . [b₁,i])) where b₂ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₂ in S } ,(RealPoset [.0,1.]))) where b₁ is Element of X : verum } is set
"\/" ( { ("\/" ( { ((R . [t,b₁]) "/\" (b₂ . [b₁,i])) where b₂ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₂ in S } ,(RealPoset [.0,1.]))) where b₁ is Element of X : verum } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
{ ("\/" ( { ((R . [t,b₂]) "/\" (b₁ . [b₂,i])) where b₂ is Element of X : verum } ,(RealPoset [.0,1.]))) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } is set
"\/" ( { ("\/" ( { ((R . [t,b₂]) "/\" (b₁ . [b₂,i])) where b₂ is Element of X : verum } ,(RealPoset [.0,1.]))) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
{ ("\/" ( { ((R . [t,b₂]) "/\" ((@ b₁) . [b₂,i])) where b₂ is Element of X : verum } ,(RealPoset [.0,1.]))) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } is set
"\/" ( { ("\/" ( { ((R . [t,b₂]) "/\" ((@ b₁) . [b₂,i])) where b₂ is Element of X : verum } ,(RealPoset [.0,1.]))) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[t,i] is Element of [:X,X:]
{ ((R (#) (@ b₁)) . [t,i]) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } is set
"\/" ( { ((R (#) (@ b₁)) . [t,i]) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
pi ( { (R (#) (@ b₁)) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } ,[t,i]) is set
"\/" ((pi ( { (R (#) (@ b₁)) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } ,[t,i])),(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
FuzzyLattice [:X,X:] is non empty V138() reflexive transitive antisymmetric with_suprema with_infima complete Heyting L14()
the carrier of (FuzzyLattice [:X,X:]) is non empty set
bool the carrier of (FuzzyLattice [:X,X:]) is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
S is Element of bool the carrier of (FuzzyLattice [:X,X:])
"\/" (S,(FuzzyLattice [:X,X:])) is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
@ ("\/" (S,(FuzzyLattice [:X,X:]))) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(@ ("\/" (S,(FuzzyLattice [:X,X:])))) (#) R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
{ ((@ b₁) (#) R) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } is set
"\/" ( { ((@ b₁) (#) R) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } ,(FuzzyLattice [:X,X:])) is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
@ ("\/" ( { ((@ b₁) (#) R) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } ,(FuzzyLattice [:X,X:]))) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
c is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
t is Element of X
i is Element of X
((@ ("\/" (S,(FuzzyLattice [:X,X:])))) (#) R) . (t,i) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[t,i] is set
{t,i} is non empty set
{t} is non empty set
{{t,i},{t}} is non empty set
((@ ("\/" (S,(FuzzyLattice [:X,X:])))) (#) R) . [t,i] is set
c . (t,i) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
c . [t,i] is set
n is set
j is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
@ j is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(@ j) (#) R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
([:X,X:],((@ j) (#) R)) @ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
{ (("\/" ((pi (S,[t,b₁])),(RealPoset [.0,1.]))) "/\" (R . [b₁,i])) where b₁ is Element of X : verum } is set
{ ("\/" ( { (b₂ "/\" (R . [b₁,i])) where b₂ is V24() ext-real real Element of the carrier of (RealPoset [.0,1.]) : b₂ in pi (S,[t,b₁]) } ,(RealPoset [.0,1.]))) where b₁ is Element of X : verum } is set
{ (b₁ "/\" (R . [a₁,i])) where b₁ is V24() ext-real real Element of the carrier of (RealPoset [.0,1.]) : b₁ in pi (S,[t,a₁]) } is set
"\/" ( { (b₁ "/\" (R . [a₁,i])) where b₁ is V24() ext-real real Element of the carrier of (RealPoset [.0,1.]) : b₁ in pi (S,[t,a₁]) } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(RealPoset [.0,1.]) |^ [:X,X:] is non empty V183() reflexive transitive antisymmetric with_suprema with_infima complete Heyting L14()
[:X,X:] --> (RealPoset [.0,1.]) is non empty Relation-like [:X,X:] -defined {(RealPoset [.0,1.])} -valued Function-like total quasi_total V197() V201() V202() Element of bool [:[:X,X:],{(RealPoset [.0,1.])}:]
{(RealPoset [.0,1.])} is non empty set
[:[:X,X:],{(RealPoset [.0,1.])}:] is non empty Relation-like set
bool [:[:X,X:],{(RealPoset [.0,1.])}:] is non empty set
product ([:X,X:] --> (RealPoset [.0,1.])) is V183() L14()
the carrier of (product ([:X,X:] --> (RealPoset [.0,1.]))) is set
bool the carrier of (product ([:X,X:] --> (RealPoset [.0,1.]))) is non empty set
j is Element of X
[t,j] is Element of [:X,X:]
{t,j} is non empty set
{{t,j},{t}} is non empty set
pi (S,[t,j]) is set
"\/" ((pi (S,[t,j])),(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[j,i] is Element of [:X,X:]
{j,i} is non empty set
{j} is non empty set
{{j,i},{j}} is non empty set
R . [j,i] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
("\/" ((pi (S,[t,j])),(RealPoset [.0,1.]))) "/\" (R . [j,i]) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min (("\/" ((pi (S,[t,j])),(RealPoset [.0,1.]))),(R . [j,i])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
{ (b₁ "/\" (R . [j,i])) where b₁ is V24() ext-real real Element of the carrier of (RealPoset [.0,1.]) : b₁ in pi (S,[t,j]) } is set
"\/" ( { (b₁ "/\" (R . [j,i])) where b₁ is V24() ext-real real Element of the carrier of (RealPoset [.0,1.]) : b₁ in pi (S,[t,j]) } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
n is Element of bool the carrier of (product ([:X,X:] --> (RealPoset [.0,1.])))
pi (n,[t,j]) is Element of bool the carrier of (([:X,X:] --> (RealPoset [.0,1.])) . [t,j])
([:X,X:] --> (RealPoset [.0,1.])) . [t,j] is L14()
the carrier of (([:X,X:] --> (RealPoset [.0,1.])) . [t,j]) is set
bool the carrier of (([:X,X:] --> (RealPoset [.0,1.])) . [t,j]) is non empty set
bool the carrier of (RealPoset [.0,1.]) is non empty set
n is Element of X
[t,n] is Element of [:X,X:]
{t,n} is non empty set
{{t,n},{t}} is non empty set
pi (S,[t,n]) is set
"\/" ((pi (S,[t,n])),(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[n,i] is Element of [:X,X:]
{n,i} is non empty set
{n} is non empty set
{{n,i},{n}} is non empty set
R . [n,i] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
("\/" ((pi (S,[t,n])),(RealPoset [.0,1.]))) "/\" (R . [n,i]) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min (("\/" ((pi (S,[t,n])),(RealPoset [.0,1.]))),(R . [n,i])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
{ (b₁ "/\" (R . [n,i])) where b₁ is V24() ext-real real Element of the carrier of (RealPoset [.0,1.]) : b₁ in pi (S,[t,n]) } is set
"\/" ( { (b₁ "/\" (R . [n,i])) where b₁ is V24() ext-real real Element of the carrier of (RealPoset [.0,1.]) : b₁ in pi (S,[t,n]) } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
{ H₂(b₁) where b₁ is Element of X : S₁[b₁] } is set
{ H₁(b₁) where b₁ is Element of X : S₁[b₁] } is set
{ ("\/" ( { ((b₂ . [t,b₁]) "/\" (R . [b₁,i])) where b₂ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₂ in S } ,(RealPoset [.0,1.]))) where b₁ is Element of X : verum } is set
{ ((b₁ . [t,a₁]) "/\" (R . [a₁,i])) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } is set
"\/" ( { ((b₁ . [t,a₁]) "/\" (R . [a₁,i])) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
{ (b₁ "/\" (R . [a₁,i])) where b₁ is V24() ext-real real Element of the carrier of (RealPoset [.0,1.]) : b₁ in pi (S,[t,a₁]) } is set
"\/" ( { (b₁ "/\" (R . [a₁,i])) where b₁ is V24() ext-real real Element of the carrier of (RealPoset [.0,1.]) : b₁ in pi (S,[t,a₁]) } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
n is Element of X
[n,i] is Element of [:X,X:]
{n,i} is non empty set
{n} is non empty set
{{n,i},{n}} is non empty set
R . [n,i] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[t,n] is Element of [:X,X:]
{t,n} is non empty set
{{t,n},{t}} is non empty set
pi (S,[t,n]) is set
{ (b₁ "/\" (R . [n,i])) where b₁ is V24() ext-real real Element of the carrier of (RealPoset [.0,1.]) : b₁ in pi (S,[t,n]) } is set
"\/" ( { (b₁ "/\" (R . [n,i])) where b₁ is V24() ext-real real Element of the carrier of (RealPoset [.0,1.]) : b₁ in pi (S,[t,n]) } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
{ ((b₁ . [t,n]) "/\" (R . [n,i])) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } is set
"\/" ( { ((b₁ . [t,n]) "/\" (R . [n,i])) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
f is set
b is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
b . [t,n] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(b . [t,n]) "/\" (R . [n,i]) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min ((b . [t,n]),(R . [n,i])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
f is set
b is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
b "/\" (R . [n,i]) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min (b,(R . [n,i])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
c₁₄ is Relation-like Function-like set
c₁₄ . [t,n] is set
n is Element of X
[n,i] is Element of [:X,X:]
{n,i} is non empty set
{n} is non empty set
{{n,i},{n}} is non empty set
R . [n,i] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[t,n] is Element of [:X,X:]
{t,n} is non empty set
{{t,n},{t}} is non empty set
pi (S,[t,n]) is set
{ (b₁ "/\" (R . [n,i])) where b₁ is V24() ext-real real Element of the carrier of (RealPoset [.0,1.]) : b₁ in pi (S,[t,n]) } is set
"\/" ( { (b₁ "/\" (R . [n,i])) where b₁ is V24() ext-real real Element of the carrier of (RealPoset [.0,1.]) : b₁ in pi (S,[t,n]) } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
{ ((b₁ . [t,n]) "/\" (R . [n,i])) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } is set
"\/" ( { ((b₁ . [t,n]) "/\" (R . [n,i])) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
{ H₂(b₁) where b₁ is Element of X : S₁[b₁] } is set
{ H₁(b₁) where b₁ is Element of X : S₁[b₁] } is set
"\/" ( { ("\/" ( { ((b₂ . [t,b₁]) "/\" (R . [b₁,i])) where b₂ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₂ in S } ,(RealPoset [.0,1.]))) where b₁ is Element of X : verum } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
{ ("\/" ( { ((b₁ . [t,b₂]) "/\" (R . [b₂,i])) where b₂ is Element of X : verum } ,(RealPoset [.0,1.]))) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } is set
"\/" ( { ("\/" ( { ((b₁ . [t,b₂]) "/\" (R . [b₂,i])) where b₂ is Element of X : verum } ,(RealPoset [.0,1.]))) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
j is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
n is Element of X
[t,n] is Element of [:X,X:]
{t,n} is non empty set
{{t,n},{t}} is non empty set
j . [t,n] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[n,i] is Element of [:X,X:]
{n,i} is non empty set
{n} is non empty set
{{n,i},{n}} is non empty set
R . [n,i] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(j . [t,n]) "/\" (R . [n,i]) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min ((j . [t,n]),(R . [n,i])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
{ ("\/" ( { H₂(b₁,b₂) where b₂ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : S₁[b₂] } ,(RealPoset [.0,1.]))) where b₁ is Element of X : S₂[b₁] } is set
"\/" ( { ("\/" ( { H₂(b₁,b₂) where b₂ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : S₁[b₂] } ,(RealPoset [.0,1.]))) where b₁ is Element of X : S₂[b₁] } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
{ ("\/" ( { H₁(b₂,b₁) where b₂ is Element of X : S₂[b₂] } ,(RealPoset [.0,1.]))) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : S₁[b₁] } is set
"\/" ( { ("\/" ( { H₁(b₂,b₁) where b₂ is Element of X : S₂[b₂] } ,(RealPoset [.0,1.]))) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : S₁[b₁] } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
{ ("\/" ( { (((@ b₁) . [t,b₂]) "/\" (R . [b₂,i])) where b₂ is Element of X : verum } ,(RealPoset [.0,1.]))) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } is set
{ (((@ a₁) . [t,b₁]) "/\" (R . [b₁,i])) where b₁ is Element of X : verum } is set
"\/" ( { (((@ a₁) . [t,b₁]) "/\" (R . [b₁,i])) where b₁ is Element of X : verum } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
{ ((a₁ . [t,b₁]) "/\" (R . [b₁,i])) where b₁ is Element of X : verum } is set
"\/" ( { ((a₁ . [t,b₁]) "/\" (R . [b₁,i])) where b₁ is Element of X : verum } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
n is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
{ ((n . [t,b₁]) "/\" (R . [b₁,i])) where b₁ is Element of X : verum } is set
"\/" ( { ((n . [t,b₁]) "/\" (R . [b₁,i])) where b₁ is Element of X : verum } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
@ n is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
{ (((@ n) . [t,b₁]) "/\" (R . [b₁,i])) where b₁ is Element of X : verum } is set
"\/" ( { (((@ n) . [t,b₁]) "/\" (R . [b₁,i])) where b₁ is Element of X : verum } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
j is Element of X
[t,j] is Element of [:X,X:]
{t,j} is non empty set
{{t,j},{t}} is non empty set
n . [t,j] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[j,i] is Element of [:X,X:]
{j,i} is non empty set
{j} is non empty set
{{j,i},{j}} is non empty set
R . [j,i] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(n . [t,j]) "/\" (R . [j,i]) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min ((n . [t,j]),(R . [j,i])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(@ n) . [t,j] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
((@ n) . [t,j]) "/\" (R . [j,i]) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min (((@ n) . [t,j]),(R . [j,i])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
{ H₄(b₁) where b₁ is Element of X : S₂[b₁] } is set
{ H₃(b₁) where b₁ is Element of X : S₂[b₁] } is set
n is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
{ ((n . [t,b₁]) "/\" (R . [b₁,i])) where b₁ is Element of X : verum } is set
"\/" ( { ((n . [t,b₁]) "/\" (R . [b₁,i])) where b₁ is Element of X : verum } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
@ n is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
{ (((@ n) . [t,b₁]) "/\" (R . [b₁,i])) where b₁ is Element of X : verum } is set
"\/" ( { (((@ n) . [t,b₁]) "/\" (R . [b₁,i])) where b₁ is Element of X : verum } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
{ H₂(b₁) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : S₁[b₁] } is set
{ H₁(b₁) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : S₁[b₁] } is set
[t,i] is Element of [:X,X:]
{ (((@ b₁) (#) R) . [t,i]) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } is set
pi ( { ((@ b₁) (#) R) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in S } ,[t,i]) is set
f is set
f is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
@ f is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(@ f) (#) R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
((@ f) (#) R) . [t,i] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
f is set
f is Relation-like Function-like set
f . [t,i] is set
b is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
@ b is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(@ b) (#) R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
{ (((@ ("\/" (S,(FuzzyLattice [:X,X:])))) . [t,b₁]) "/\" (R . [b₁,i])) where b₁ is Element of X : verum } is set
n is Element of X
[t,n] is Element of [:X,X:]
{t,n} is non empty set
{{t,n},{t}} is non empty set
(@ ("\/" (S,(FuzzyLattice [:X,X:])))) . [t,n] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[n,i] is Element of [:X,X:]
{n,i} is non empty set
{n} is non empty set
{{n,i},{n}} is non empty set
R . [n,i] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
((@ ("\/" (S,(FuzzyLattice [:X,X:])))) . [t,n]) "/\" (R . [n,i]) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min (((@ ("\/" (S,(FuzzyLattice [:X,X:])))) . [t,n]),(R . [n,i])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
pi (S,[t,n]) is set
"\/" ((pi (S,[t,n])),(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
("\/" ((pi (S,[t,n])),(RealPoset [.0,1.]))) "/\" (R . [n,i]) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min (("\/" ((pi (S,[t,n])),(RealPoset [.0,1.]))),(R . [n,i])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
("\/" (S,(FuzzyLattice [:X,X:]))) . [t,n] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
n is Element of X
[t,n] is Element of [:X,X:]
{t,n} is non empty set
{{t,n},{t}} is non empty set
(@ ("\/" (S,(FuzzyLattice [:X,X:])))) . [t,n] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
[n,i] is Element of [:X,X:]
{n,i} is non empty set
{n} is non empty set
{{n,i},{n}} is non empty set
R . [n,i] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
((@ ("\/" (S,(FuzzyLattice [:X,X:])))) . [t,n]) "/\" (R . [n,i]) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min (((@ ("\/" (S,(FuzzyLattice [:X,X:])))) . [t,n]),(R . [n,i])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
pi (S,[t,n]) is set
"\/" ((pi (S,[t,n])),(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
("\/" ((pi (S,[t,n])),(RealPoset [.0,1.]))) "/\" (R . [n,i]) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
min (("\/" ((pi (S,[t,n])),(RealPoset [.0,1.]))),(R . [n,i])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
{ H₂(b₁) where b₁ is Element of X : S₁[b₁] } is set
{ H₁(b₁) where b₁ is Element of X : S₁[b₁] } is set
{ (((@ a₁) . [t,b₁]) "/\" (R . [b₁,i])) where b₁ is Element of X : verum } is set
"\/" ( { (((@ a₁) . [t,b₁]) "/\" (R . [b₁,i])) where b₁ is Element of X : verum } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
n is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
@ n is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
{ (((@ n) . [t,b₁]) "/\" (R . [b₁,i])) where b₁ is Element of X : verum } is set
"\/" ( { (((@ n) . [t,b₁]) "/\" (R . [b₁,i])) where b₁ is Element of X : verum } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(@ n) (#) R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
((@ n) (#) R) . [t,i] is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
{ H₂(b₁) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : S₁[b₁] } is set
{ H₁(b₁) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : S₁[b₁] } is set
"\/" ( { (((@ ("\/" (S,(FuzzyLattice [:X,X:])))) . [t,b₁]) "/\" (R . [b₁,i])) where b₁ is Element of X : verum } ,(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
FuzzyLattice [:X,X:] is non empty V138() reflexive transitive antisymmetric with_suprema with_infima complete Heyting L14()
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,R) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
{ (X,R,b₁) where b₁ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } is set
"\/" ( { (X,R,b₁) where b₁ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } ,(FuzzyLattice [:X,X:])) is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
the carrier of (FuzzyLattice [:X,X:]) is non empty set
(X,R) (#) (X,R) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
{ ((X,R,b₁) (#) (X,R,b₂)) where b₁, b₂ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : ( not b₁ <= 0 & not b₂ <= 0 ) } is set
"\/" ( { ((X,R,b₁) (#) (X,R,b₂)) where b₁, b₂ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : ( not b₁ <= 0 & not b₂ <= 0 ) } ,(FuzzyLattice [:X,X:])) is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
RP is set
c is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT
(X,R,c) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
([:X,X:],(X,R,c)) @ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
{ ("\/" ( { ((@ b₁) (#) (@ b₂)) where b₂ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₂ in { (X,R,b₁) where b₃ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } } ,(FuzzyLattice [:X,X:]))) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in { (X,R,b₁) where b₂ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } } is set
{ ("\/" ( { (([:X,X:],((@ b₁) (#) (@ b₂))) @) where b₂ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₂ in { (X,R,b₁) where b₃ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } } ,(FuzzyLattice [:X,X:]))) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in { (X,R,b₁) where b₂ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } } is set
{ (([:X,X:],((@ a₁) (#) (@ b₁))) @) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in { (X,R,b₁) where b₂ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } } is set
"\/" ( { (([:X,X:],((@ a₁) (#) (@ b₁))) @) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in { (X,R,b₁) where b₂ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } } ,(FuzzyLattice [:X,X:])) is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
{ ((@ a₁) (#) (@ b₁)) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in { (X,R,b₁) where b₂ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } } is set
"\/" ( { ((@ a₁) (#) (@ b₁)) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in { (X,R,b₁) where b₂ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } } ,(FuzzyLattice [:X,X:])) is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
RP is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
@ RP is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
{ ((@ RP) (#) (@ b₁)) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in { (X,R,b₁) where b₂ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } } is set
"\/" ( { ((@ RP) (#) (@ b₁)) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in { (X,R,b₁) where b₂ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } } ,(FuzzyLattice [:X,X:])) is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
{ (([:X,X:],((@ RP) (#) (@ b₁))) @) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in { (X,R,b₁) where b₂ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } } is set
"\/" ( { (([:X,X:],((@ RP) (#) (@ b₁))) @) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in { (X,R,b₁) where b₂ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } } ,(FuzzyLattice [:X,X:])) is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
c is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
@ c is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(@ RP) (#) (@ c) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
([:X,X:],((@ RP) (#) (@ c))) @ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
{ H₄(b₁) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : S₂[b₁] } is set
{ H₃(b₁) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : S₂[b₁] } is set
RP is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
@ RP is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
{ ((@ RP) (#) (@ b₁)) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in { (X,R,b₁) where b₂ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } } is set
"\/" ( { ((@ RP) (#) (@ b₁)) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in { (X,R,b₁) where b₂ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } } ,(FuzzyLattice [:X,X:])) is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
{ (([:X,X:],((@ RP) (#) (@ b₁))) @) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in { (X,R,b₁) where b₂ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } } is set
"\/" ( { (([:X,X:],((@ RP) (#) (@ b₁))) @) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in { (X,R,b₁) where b₂ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } } ,(FuzzyLattice [:X,X:])) is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
{ H₂(b₁) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : S₁[b₁] } is set
{ H₁(b₁) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : S₁[b₁] } is set
{ ((@ b₁) (#) (@ b₂)) where b₁, b₂ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : ( b₁ in { (X,R,b₁) where b₃ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } & b₂ in { (X,R,b₁) where b₃ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } ) } is set
t is set
i is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
@ i is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
n is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
@ n is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(@ i) (#) (@ n) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
j is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT
(X,R,j) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
f is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT
(X,R,f) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
t is set
i is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT
(X,R,i) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
n is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT
(X,R,n) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,R,i) (#) (X,R,n) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
([:X,X:],(X,R,n)) @ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
([:X,X:],(X,R,i)) @ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
f is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
@ f is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
j is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
@ j is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
{ (([:X,X:],((@ b₁) (#) (@ b₂))) @) where b₁, b₂ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : ( b₁ in { (X,R,b₁) where b₃ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } & b₂ in { (X,R,b₁) where b₃ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } ) } is set
RP is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
@ RP is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
c is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
@ c is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(@ RP) (#) (@ c) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
([:X,X:],((@ RP) (#) (@ c))) @ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
{ H₃(b₁,b₂) where b₁, b₂ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : S₃[b₁,b₂] } is set
{ H₂(b₁,b₂) where b₁, b₂ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : S₃[b₁,b₂] } is set
@ ("\/" ( { (X,R,b₁) where b₁ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } ,(FuzzyLattice [:X,X:]))) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
{ ((@ b₁) (#) (X,R)) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in { (X,R,b₁) where b₂ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } } is set
t is set
i is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
@ i is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(@ i) (#) (X,R) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
{ ((@ i) (#) (@ b₁)) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in { (X,R,b₁) where b₂ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } } is set
"\/" ( { ((@ i) (#) (@ b₁)) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in { (X,R,b₁) where b₂ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } } ,(FuzzyLattice [:X,X:])) is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
t is set
i is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
@ i is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
{ ((@ i) (#) (@ b₁)) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in { (X,R,b₁) where b₂ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } } is set
"\/" ( { ((@ i) (#) (@ b₁)) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : b₁ in { (X,R,b₁) where b₂ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } } ,(FuzzyLattice [:X,X:])) is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
(@ i) (#) (X,R) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
{ ("\/" ( { H₁(b₁,b₂) where b₂ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : S₁[b₂] } ,(FuzzyLattice [:X,X:]))) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : S₂[b₁] } is set
"\/" ( { ("\/" ( { H₁(b₁,b₂) where b₂ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : S₁[b₂] } ,(FuzzyLattice [:X,X:]))) where b₁ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : S₂[b₁] } ,(FuzzyLattice [:X,X:])) is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
{ H₁(b₁,b₂) where b₁, b₂ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : ( S₂[b₁] & S₁[b₂] ) } is set
"\/" ( { H₁(b₁,b₂) where b₁, b₂ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:]) : ( S₂[b₁] & S₁[b₂] ) } ,(FuzzyLattice [:X,X:])) is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,R) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
FuzzyLattice [:X,X:] is non empty V138() reflexive transitive antisymmetric with_suprema with_infima complete Heyting L14()
{ (X,R,b₁) where b₁ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } is set
"\/" ( { (X,R,b₁) where b₁ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } ,(FuzzyLattice [:X,X:])) is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
the carrier of (FuzzyLattice [:X,X:]) is non empty set
{ ((X,R,b₁) (#) (X,R,b₂)) where b₁, b₂ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : ( not b₁ <= 0 & not b₂ <= 0 ) } is set
(X,R) (#) (X,R) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
c is Element of [:X,X:]
((X,R) (#) (X,R)) . c is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(X,R) . c is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
t is set
i is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT
(X,R,i) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
n is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT
(X,R,n) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,R,i) (#) (X,R,n) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
([:X,X:],((X,R,i) (#) (X,R,n))) @ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
pi ( { ((X,R,b₁) (#) (X,R,b₂)) where b₁, b₂ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : ( not b₁ <= 0 & not b₂ <= 0 ) } ,c) is set
t is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
i is Relation-like Function-like set
i . c is set
n is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT
(X,R,n) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
j is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT
(X,R,j) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,R,n) (#) (X,R,j) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
n + j is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT
(X,R,(n + j)) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
f is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
f . c is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
"\/" ((pi ( { ((X,R,b₁) (#) (X,R,b₂)) where b₁, b₂ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : ( not b₁ <= 0 & not b₂ <= 0 ) } ,c)),(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
"\/" ( { ((X,R,b₁) (#) (X,R,b₂)) where b₁, b₂ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : ( not b₁ <= 0 & not b₂ <= 0 ) } ,(FuzzyLattice [:X,X:])) is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
("\/" ( { ((X,R,b₁) (#) (X,R,b₂)) where b₁, b₂ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : ( not b₁ <= 0 & not b₂ <= 0 ) } ,(FuzzyLattice [:X,X:]))) . c is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
S is ordinal natural V24() ext-real non negative real set
(X,R,S) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
R (#) R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
RP is non empty ordinal natural V24() ext-real positive non negative real set
(X,R,RP) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
RP + 1 is non empty ordinal natural V24() ext-real positive non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT
(X,R,(RP + 1)) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,R,RP) (#) R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,R,1) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
Q is non empty ordinal natural V24() ext-real positive non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT
(X,R,Q) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,R) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued (X) Element of bool [:[:X,X:],REAL:]
FuzzyLattice [:X,X:] is non empty V138() reflexive transitive antisymmetric with_suprema with_infima complete Heyting L14()
{ (X,R,b₁) where b₁ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } is set
"\/" ( { (X,R,b₁) where b₁ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } ,(FuzzyLattice [:X,X:])) is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
the carrier of (FuzzyLattice [:X,X:]) is non empty set
RP is Element of [:X,X:]
(X,R) . RP is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
R . RP is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
pi ( { (X,R,b₁) where b₁ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } ,RP) is set
c is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
t is Relation-like Function-like set
t . RP is set
i is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT
(X,R,i) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,R,i) . RP is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
c is set
t is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT
(X,R,t) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
([:X,X:],(X,R,t)) @ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
"\/" ((pi ( { (X,R,b₁) where b₁ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } ,RP)),(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
S is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
Q is ordinal natural V24() ext-real non negative real set
(X,R,Q) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,S,Q) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
RP is ordinal natural V24() ext-real non negative real set
(X,R,RP) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,S,RP) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
RP + 1 is non empty ordinal natural V24() ext-real positive non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT
(X,R,(RP + 1)) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,S,(RP + 1)) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,R,RP) (#) R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,S,RP) (#) S is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,R,0) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
Imf (X,X) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued (X) (X) (X) (X) Element of bool [:[:X,X:],REAL:]
(X,S,0) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
X is non empty set
[:X,X:] is non empty Relation-like set
[:[:X,X:],REAL:] is non empty Relation-like set
bool [:[:X,X:],REAL:] is non empty set
S is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
R is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,R) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued (X) Element of bool [:[:X,X:],REAL:]
FuzzyLattice [:X,X:] is non empty V138() reflexive transitive antisymmetric with_suprema with_infima complete Heyting L14()
{ (X,R,b₁) where b₁ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } is set
"\/" ( { (X,R,b₁) where b₁ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } ,(FuzzyLattice [:X,X:])) is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
the carrier of (FuzzyLattice [:X,X:]) is non empty set
(X,S) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued (X) Element of bool [:[:X,X:],REAL:]
{ (X,S,b₁) where b₁ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } is set
"\/" ( { (X,S,b₁) where b₁ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } ,(FuzzyLattice [:X,X:])) is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])
c is Element of [:X,X:]
(X,R) . c is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
(X,S) . c is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
pi ( { (X,R,b₁) where b₁ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } ,c) is set
t is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
i is Relation-like Function-like set
i . c is set
n is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT
(X,R,n) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,S,n) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
(X,R,n) . c is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
"\/" ((pi ( { (X,R,b₁) where b₁ is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT : not b₁ <= 0 } ,c)),(RealPoset [.0,1.])) is V24() ext-real real Element of the carrier of (RealPoset [.0,1.])
t is set
i is ordinal natural V24() ext-real non negative real V43() V44() V45() V46() V47() V48() V50() V51() Element of NAT
(X,R,i) is non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued Element of bool [:[:X,X:],REAL:]
([:X,X:],(X,R,i)) @ is Relation-like Function-like Element of the carrier of (FuzzyLattice [:X,X:])