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: b 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: b 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