Nuprl Definition : sub-co-list
sub-co-list(T;s1;s2) == ∃ns:colist(ℕ). (s1 = s2@ns ∈ colist(T))
Definitions occuring in Statement :
list-at: L1@L2,
colist: colist(T),
nat: ℕ,
exists: ∃x:A. B[x],
equal: s = t ∈ T
Definitions occuring in definition :
exists: ∃x:A. B[x],
nat: ℕ,
equal: s = t ∈ T,
colist: colist(T),
list-at: L1@L2
FDL editor aliases :
sub-co-list
Latex:
sub-co-list(T;s1;s2) == \mexists{}ns:colist(\mBbbN{}). (s1 = s2@ns)
Date html generated:
2019_06_20-PM-01_21_53
Last ObjectModification:
2018_12_07-PM-06_30_49
Theory : list_1
Home
Index