Nuprl Definition : k-subtype
A ⊆ B == ∀i:ℕk. ((A i) ⊆r (B i))
Definitions occuring in Statement :
int_seg: {i..j-},
subtype_rel: A ⊆r B,
all: ∀x:A. B[x],
apply: f a,
natural_number: $n
Definitions occuring in definition :
all: ∀x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
subtype_rel: A ⊆r B,
apply: f a
FDL editor aliases :
k-subtype
Latex:
A \msubseteq{} B == \mforall{}i:\mBbbN{}k. ((A i) \msubseteq{}r (B i))
Date html generated:
2018_05_21-PM-00_08_42
Last ObjectModification:
2017_10_09-PM-05_11_21
Theory : co-recursion
Home
Index