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:
2019_06_20-PM-01_12_43
Last ObjectModification:
2019_01_02-PM-01_36_03
Theory : co-recursion-2
Home
Index