Nuprl Definition : homogeneous
homogeneous(R;n;s) ==
strictly-increasing-seq(n;s) ∧ (∀m,i,j:ℕn. (m < i ⇒ m < j ⇒ (R (s m) (s i) ⇐⇒ R (s m) (s j))))
Definitions occuring in Statement :
strictly-increasing-seq: strictly-increasing-seq(n;s),
int_seg: {i..j-},
less_than: a < b,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
natural_number: $n
Definitions occuring in definition :
and: P ∧ Q,
strictly-increasing-seq: strictly-increasing-seq(n;s),
all: ∀x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
implies: P ⇒ Q,
less_than: a < b,
iff: P ⇐⇒ Q,
apply: f a
FDL editor aliases :
homogeneous
Latex:
homogeneous(R;n;s) ==
strictly-increasing-seq(n;s) \mwedge{} (\mforall{}m,i,j:\mBbbN{}n. (m < i {}\mRightarrow{} m < j {}\mRightarrow{} (R (s m) (s i) \mLeftarrow{}{}\mRightarrow{} R (s m) (s j))))
Date html generated:
2016_05_13-PM-03_50_03
Last ObjectModification:
2015_09_22-PM-05_45_20
Theory : bar-induction
Home
Index