Nuprl Definition : k-monotone

k-Monotone(T.F[T]) ==  ∀[A,B:ℕk ⟶ Type].  F[A] ⊆ F[B] supposing A ⊆ B



Definitions occuring in Statement :  k-subtype: A ⊆ B int_seg: {i..j-} uimplies: supposing a uall: [x:A]. B[x] function: x:A ⟶ B[x] natural_number: $n universe: Type
Definitions occuring in definition :  uall: [x:A]. B[x] function: x:A ⟶ B[x] int_seg: {i..j-} natural_number: $n universe: Type uimplies: supposing a k-subtype: A ⊆ B
FDL editor aliases :  k-monotone

Latex:
k-Monotone(T.F[T])  ==    \mforall{}[A,B:\mBbbN{}k  {}\mrightarrow{}  Type].    F[A]  \msubseteq{}  F[B]  supposing  A  \msubseteq{}  B



Date html generated: 2018_05_21-PM-00_09_06
Last ObjectModification: 2017_10_18-PM-02_33_02

Theory : co-recursion


Home Index