Nuprl Definition : almost-full
AFx,y:T.R[x; y] == ∀f:ℕ ⟶ T. (↓∃i,j:ℕ. (i < j ∧ R[f i; f j]))
Definitions occuring in Statement :
nat: ℕ,
less_than: a < b,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
squash: ↓T,
and: P ∧ Q,
apply: f a,
function: x:A ⟶ B[x]
Definitions occuring in definition :
all: ∀x:A. B[x],
function: x:A ⟶ B[x],
squash: ↓T,
exists: ∃x:A. B[x],
nat: ℕ,
and: P ∧ Q,
less_than: a < b,
apply: f a
FDL editor aliases :
almost-full
Latex:
AFx,y:T.R[x; y] == \mforall{}f:\mBbbN{} {}\mrightarrow{} T. (\mdownarrow{}\mexists{}i,j:\mBbbN{}. (i < j \mwedge{} R[f i; f j]))
Date html generated:
2016_05_13-PM-03_50_52
Last ObjectModification:
2015_09_22-PM-05_45_22
Theory : bar-induction
Home
Index