Nuprl Definition : family-monotone
family-monotone{i:l}(P;H) == ∀F,G:P ⟶ Type. (F ⊆ G ⇒ H F ⊆ H G)
Definitions occuring in Statement :
sub-family: F ⊆ G,
all: ∀x:A. B[x],
implies: P ⇒ Q,
apply: f a,
function: x:A ⟶ B[x],
universe: Type
Definitions occuring in definition :
all: ∀x:A. B[x],
function: x:A ⟶ B[x],
universe: Type,
implies: P ⇒ Q,
sub-family: F ⊆ G,
apply: f a
FDL editor aliases :
family-monotone
Latex:
family-monotone\{i:l\}(P;H) == \mforall{}F,G:P {}\mrightarrow{} Type. (F \msubseteq{} G {}\mRightarrow{} H F \msubseteq{} H G)
Date html generated:
2016_05_14-AM-06_12_14
Last ObjectModification:
2015_09_22-PM-05_46_58
Theory : co-recursion
Home
Index