Nuprl Definition : bounded-type
Bounded(T) == ∀K:T ⟶ ℕ. (∃B:ℕ [(∀t:T. ((K t) ≤ B))])
Definitions occuring in Statement :
nat: ℕ,
le: A ≤ B,
all: ∀x:A. B[x],
sq_exists: ∃x:A [B[x]],
apply: f a,
function: x:A ⟶ B[x]
Definitions occuring in definition :
apply: f a,
le: A ≤ B,
all: ∀x:A. B[x],
nat: ℕ,
sq_exists: ∃x:A [B[x]],
function: x:A ⟶ B[x]
FDL editor aliases :
bounded-type
bounded-type
Latex:
Bounded(T) == \mforall{}K:T {}\mrightarrow{} \mBbbN{}. (\mexists{}B:\mBbbN{} [(\mforall{}t:T. ((K t) \mleq{} B))])
Date html generated:
2019_10_15-AM-10_20_05
Last ObjectModification:
2019_10_07-PM-04_38_16
Theory : bar-induction
Home
Index