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: 2019_06_20-PM-01_12_38
Last ObjectModification: 2019_01_02-PM-01_35_54

Theory : co-recursion-2


Home Index