Nuprl Definition : alt-int-rdiv
alt-int-rdiv(x;k) == if k=1 then x else (λn.[x n ÷ k])
Definitions occuring in Statement :
rounding-div: [b ÷ m],
int_eq: if a=b then c else d,
apply: f a,
lambda: λx.A[x],
natural_number: $n
Definitions occuring in definition :
int_eq: if a=b then c else d,
natural_number: $n,
lambda: λx.A[x],
rounding-div: [b ÷ m],
apply: f a
FDL editor aliases :
alt-int-rdiv
Latex:
alt-int-rdiv(x;k) == if k=1 then x else (\mlambda{}n.[x n \mdiv{} k])
Date html generated:
2019_10_29-AM-09_33_15
Last ObjectModification:
2019_02_18-PM-00_07_20
Theory : reals
Home
Index