Nuprl Definition : fs-in-subtype
fs-in-subtype(K;S;T;f) == fs-predicate(K;S;p.snd(p) ∈ T;f)
Definitions occuring in Statement :
fs-predicate: fs-predicate(K;S;p.P[p];f),
pi2: snd(t),
member: t ∈ T
Definitions occuring in definition :
fs-predicate: fs-predicate(K;S;p.P[p];f),
member: t ∈ T,
pi2: snd(t)
FDL editor aliases :
fs-in-subtype
Latex:
fs-in-subtype(K;S;T;f) == fs-predicate(K;S;p.snd(p) \mmember{} T;f)
Date html generated:
2019_10_31-AM-06_29_03
Last ObjectModification:
2019_08_19-PM-01_06_32
Theory : linear!algebra
Home
Index